Foundation·F07
Biconditional
A if and only if B: implication in both directions.
Defined from implication and conjunction.
In words
A if and only if B means that A implies B and B implies A.
Part of the logical framework beneath ZFC (classical first-order logic with equality): taken as given rather than proven, it belongs to the language the set-theoretic axioms are stated in.
Remarks
Purely an abbreviation, with no rules of its own. It is the workhorse of definitions: a definition on this wiki typically has the shape "the new symbol holds
some formula in old symbols", as in D001 or D005. (The metalanguage arrow
written between displayed formulas is the same idea, one level up.) In Lean, Iff is a structure bundling the two directions as .mp and .mpr.
Propose an edit3 published revisions
- 7/12/2026 · Benjamin· Split the defining conjunction into its two implications and the and symbol individually.what changed →
- 7/11/2026 · Benjamin· Fix Mathlib link: add the #doc fragment doc-gen4's find endpoint requires (old link 404'd). Content unchanged.what changed →
- 7/11/2026 · Benjamin· Logic layer: connectives and quantifierswhat changed →