P. 59 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 5801-5900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	f1ocnvfv 5801	Relationship between the value of a one-to-one onto function and the value of its converse. (Contributed by Raph Levien, 10-Apr-2004.)
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹‘𝐶) = 𝐷 → (◡𝐹‘𝐷) = 𝐶))
Theorem	f1ocnvfvb 5802	Relationship between the value of a one-to-one onto function and the value of its converse. (Contributed by NM, 20-May-2004.)
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → ((𝐹‘𝐶) = 𝐷 ↔ (◡𝐹‘𝐷) = 𝐶))
Theorem	f1ocnvdm 5803	The value of the converse of a one-to-one onto function belongs to its domain. (Contributed by NM, 26-May-2006.)
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (◡𝐹‘𝐶) ∈ 𝐴)
Theorem	f1ocnvfvrneq 5804	If the values of a one-to-one function for two arguments from the range of the function are equal, the arguments themselves must be equal. (Contributed by Alexander van der Vekens, 12-Nov-2017.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ∈ ran 𝐹 ∧ 𝐷 ∈ ran 𝐹)) → ((◡𝐹‘𝐶) = (◡𝐹‘𝐷) → 𝐶 = 𝐷))
Theorem	fcof1 5805	An application is injective if a retraction exists. Proposition 8 of [BourbakiEns] p. E.II.18. (Contributed by FL, 11-Nov-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝑅 ∘ 𝐹) = ( I ↾ 𝐴)) → 𝐹:𝐴–1-1→𝐵)
Theorem	fcofo 5806	An application is surjective if a section exists. Proposition 8 of [BourbakiEns] p. E.II.18. (Contributed by FL, 17-Nov-2011.) (Proof shortened by Mario Carneiro, 27-Dec-2014.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑆:𝐵⟶𝐴 ∧ (𝐹 ∘ 𝑆) = ( I ↾ 𝐵)) → 𝐹:𝐴–onto→𝐵)
Theorem	cbvfo 5807*	Change bound variable between domain and range of function. (Contributed by NM, 23-Feb-1997.) (Proof shortened by Mario Carneiro, 21-Mar-2015.)
⊢ ((𝐹‘𝑥) = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐹:𝐴–onto→𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓))
Theorem	cbvexfo 5808*	Change bound variable between domain and range of function. (Contributed by NM, 23-Feb-1997.)
⊢ ((𝐹‘𝑥) = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐹:𝐴–onto→𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓))
Theorem	cocan1 5809	An injection is left-cancelable. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 21-Mar-2015.)
⊢ ((𝐹:𝐵–1-1→𝐶 ∧ 𝐻:𝐴⟶𝐵 ∧ 𝐾:𝐴⟶𝐵) → ((𝐹 ∘ 𝐻) = (𝐹 ∘ 𝐾) ↔ 𝐻 = 𝐾))
Theorem	cocan2 5810	A surjection is right-cancelable. (Contributed by FL, 21-Nov-2011.) (Proof shortened by Mario Carneiro, 21-Mar-2015.)
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐻 Fn 𝐵 ∧ 𝐾 Fn 𝐵) → ((𝐻 ∘ 𝐹) = (𝐾 ∘ 𝐹) ↔ 𝐻 = 𝐾))
Theorem	fcof1o 5811	Show that two functions are inverse to each other by computing their compositions. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ (((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ((𝐹 ∘ 𝐺) = ( I ↾ 𝐵) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐴))) → (𝐹:𝐴–1-1-onto→𝐵 ∧ ◡𝐹 = 𝐺))
Theorem	foeqcnvco 5812	Condition for function equality in terms of vanishing of the composition with the converse. EDITORIAL: Is there a relation-algebraic proof of this? (Contributed by Stefan O'Rear, 12-Feb-2015.)
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) → (𝐹 = 𝐺 ↔ (𝐹 ∘ ◡𝐺) = ( I ↾ 𝐵)))
Theorem	f1eqcocnv 5813	Condition for function equality in terms of vanishing of the composition with the inverse. (Contributed by Stefan O'Rear, 12-Feb-2015.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → (𝐹 = 𝐺 ↔ (◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)))
Theorem	fliftrel 5814*	𝐹, a function lift, is a subset of 𝑅 × 𝑆. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝐹 ⊆ (𝑅 × 𝑆))
Theorem	fliftel 5815*	Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐶𝐹𝐷 ↔ ∃𝑥 ∈ 𝑋 (𝐶 = 𝐴 ∧ 𝐷 = 𝐵)))
Theorem	fliftel1 5816*	Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴𝐹𝐵)
Theorem	fliftcnv 5817*	Converse of the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ◡𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐵, 𝐴⟩))
Theorem	fliftfun 5818*	The function 𝐹 is the unique function defined by 𝐹‘𝐴 = 𝐵, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐶)    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → (Fun 𝐹 ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐴 = 𝐶 → 𝐵 = 𝐷)))
Theorem	fliftfund 5819*	The function 𝐹 is the unique function defined by 𝐹‘𝐴 = 𝐵, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐶)    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐷)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝐴 = 𝐶)) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → Fun 𝐹)
Theorem	fliftfuns 5820*	The function 𝐹 is the unique function defined by 𝐹‘𝐴 = 𝐵, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (Fun 𝐹 ↔ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵)))
Theorem	fliftf 5821*	The domain and range of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (Fun 𝐹 ↔ 𝐹:ran (𝑥 ∈ 𝑋 ↦ 𝐴)⟶𝑆))
Theorem	fliftval 5822*	The value of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆)    &   ⊢ (𝑥 = 𝑌 → 𝐴 = 𝐶)    &   ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷)    &   ⊢ (𝜑 → Fun 𝐹)    ⇒   ⊢ ((𝜑 ∧ 𝑌 ∈ 𝑋) → (𝐹‘𝐶) = 𝐷)
Theorem	isoeq1 5823	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
⊢ (𝐻 = 𝐺 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵)))
Theorem	isoeq2 5824	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
⊢ (𝑅 = 𝑇 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑇, 𝑆 (𝐴, 𝐵)))
Theorem	isoeq3 5825	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
⊢ (𝑆 = 𝑇 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑇 (𝐴, 𝐵)))
Theorem	isoeq4 5826	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
⊢ (𝐴 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐶, 𝐵)))
Theorem	isoeq5 5827	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
⊢ (𝐵 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐶)))
Theorem	nfiso 5828	Bound-variable hypothesis builder for an isomorphism. (Contributed by NM, 17-May-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ Ⅎ𝑥𝐻    &   ⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝑆    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
Theorem	isof1o 5829	An isomorphism is a one-to-one onto function. (Contributed by NM, 27-Apr-2004.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵)
Theorem	isorel 5830	An isomorphism connects binary relations via its function values. (Contributed by NM, 27-Apr-2004.)
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶𝑅𝐷 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝐷)))
Theorem	isoresbr 5831*	A consequence of isomorphism on two relations for a function's restriction. (Contributed by Jim Kingdon, 11-Jan-2019.)
⊢ ((𝐹 ↾ 𝐴) Isom 𝑅, 𝑆 (𝐴, (𝐹 “ 𝐴)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐹‘𝑥)𝑆(𝐹‘𝑦)))
Theorem	isoid 5832	Identity law for isomorphism. Proposition 6.30(1) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.)
⊢ ( I ↾ 𝐴) Isom 𝑅, 𝑅 (𝐴, 𝐴)
Theorem	isocnv 5833	Converse law for isomorphism. Proposition 6.30(2) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → ◡𝐻 Isom 𝑆, 𝑅 (𝐵, 𝐴))
Theorem	isocnv2 5834	Converse law for isomorphism. (Contributed by Mario Carneiro, 30-Jan-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom ◡𝑅, ◡𝑆(𝐴, 𝐵))
Theorem	isores2 5835	An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, (𝑆 ∩ (𝐵 × 𝐵))(𝐴, 𝐵))
Theorem	isores1 5836	An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom (𝑅 ∩ (𝐴 × 𝐴)), 𝑆(𝐴, 𝐵))
Theorem	isores3 5837	Induced isomorphism on a subset. (Contributed by Stefan O'Rear, 5-Nov-2014.)
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐾 ⊆ 𝐴 ∧ 𝑋 = (𝐻 “ 𝐾)) → (𝐻 ↾ 𝐾) Isom 𝑅, 𝑆 (𝐾, 𝑋))
Theorem	isotr 5838	Composition (transitive) law for isomorphism. Proposition 6.30(3) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐺 Isom 𝑆, 𝑇 (𝐵, 𝐶)) → (𝐺 ∘ 𝐻) Isom 𝑅, 𝑇 (𝐴, 𝐶))
Theorem	iso0 5839	The empty set is an 𝑅, 𝑆 isomorphism from the empty set to the empty set. (Contributed by Steve Rodriguez, 24-Oct-2015.)
⊢ ∅ Isom 𝑅, 𝑆 (∅, ∅)
Theorem	isoini 5840	Isomorphisms preserve initial segments. Proposition 6.31(2) of [TakeutiZaring] p. 33. (Contributed by NM, 20-Apr-2004.)
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐷 ∈ 𝐴) → (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝐷}))) = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝐷)})))
Theorem	isoini2 5841	Isomorphisms are isomorphisms on their initial segments. (Contributed by Mario Carneiro, 29-Mar-2014.)
⊢ 𝐶 = (𝐴 ∩ (◡𝑅 “ {𝑋}))    &   ⊢ 𝐷 = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑋)}))    ⇒   ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → (𝐻 ↾ 𝐶) Isom 𝑅, 𝑆 (𝐶, 𝐷))
Theorem	isoselem 5842*	Lemma for isose 5843. (Contributed by Mario Carneiro, 23-Jun-2015.)
⊢ (𝜑 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵))    &   ⊢ (𝜑 → (𝐻 “ 𝑥) ∈ V)    ⇒   ⊢ (𝜑 → (𝑅 Se 𝐴 → 𝑆 Se 𝐵))
Theorem	isose 5843	An isomorphism preserves set-like relations. (Contributed by Mario Carneiro, 23-Jun-2015.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Se 𝐴 ↔ 𝑆 Se 𝐵))
Theorem	isopolem 5844	Lemma for isopo 5845. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑆 Po 𝐵 → 𝑅 Po 𝐴))
Theorem	isopo 5845	An isomorphism preserves partial ordering. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Po 𝐴 ↔ 𝑆 Po 𝐵))
Theorem	isosolem 5846	Lemma for isoso 5847. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑆 Or 𝐵 → 𝑅 Or 𝐴))
Theorem	isoso 5847	An isomorphism preserves strict ordering. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐵))
Theorem	f1oiso 5848*	Any one-to-one onto function determines an isomorphism with an induced relation 𝑆. Proposition 6.33 of [TakeutiZaring] p. 34. (Contributed by NM, 30-Apr-2004.)
⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ 𝑆 = {⟨𝑧, 𝑤⟩ ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑧 = (𝐻‘𝑥) ∧ 𝑤 = (𝐻‘𝑦)) ∧ 𝑥𝑅𝑦)}) → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵))
Theorem	f1oiso2 5849*	Any one-to-one onto function determines an isomorphism with an induced relation 𝑆. (Contributed by Mario Carneiro, 9-Mar-2013.)
⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (◡𝐻‘𝑥)𝑅(◡𝐻‘𝑦))}    ⇒   ⊢ (𝐻:𝐴–1-1-onto→𝐵 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵))
2.6.9  Cantor's Theorem
Theorem	canth 5850	No set 𝐴 is equinumerous to its power set (Cantor's theorem), i.e., no function can map 𝐴 onto its power set. Compare Theorem 6B(b) of [Enderton] p. 132. (Use nex 1511 if you want the form ¬ ∃𝑓𝑓:𝐴–onto→𝒫 𝐴.) (Contributed by NM, 7-Aug-1994.) (Revised by Noah R Kingdon, 23-Jul-2024.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ¬ 𝐹:𝐴–onto→𝒫 𝐴
2.6.10  Restricted iota (description binder)
Syntax	crio 5851	Extend class notation with restricted description binder.
class (℩𝑥 ∈ 𝐴 𝜑)
Definition	df-riota 5852	Define restricted description binder. In case there is no unique 𝑥 such that (𝑥 ∈ 𝐴 ∧ 𝜑) holds, it evaluates to the empty set. See also comments for df-iota 5196. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 2-Sep-2018.)
⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	riotaeqdv 5853*	Formula-building deduction for iota. (Contributed by NM, 15-Sep-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐵 𝜓))
Theorem	riotabidv 5854*	Formula-building deduction for restricted iota. (Contributed by NM, 15-Sep-2011.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒))
Theorem	riotaeqbidv 5855*	Equality deduction for restricted universal quantifier. (Contributed by NM, 15-Sep-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐵 𝜒))
Theorem	riotaexg 5856*	Restricted iota is a set. (Contributed by Jim Kingdon, 15-Jun-2020.)
⊢ (𝐴 ∈ 𝑉 → (℩𝑥 ∈ 𝐴 𝜓) ∈ V)
Theorem	iotaexel 5857*	Set existence of an iota expression in which all values are contained within a set. (Contributed by Jim Kingdon, 28-Jun-2025.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥(𝜑 → 𝑥 ∈ 𝐴)) → (℩𝑥𝜑) ∈ V)
Theorem	riotav 5858	An iota restricted to the universe is unrestricted. (Contributed by NM, 18-Sep-2011.)
⊢ (℩𝑥 ∈ V 𝜑) = (℩𝑥𝜑)
Theorem	riotauni 5859	Restricted iota in terms of class union. (Contributed by NM, 11-Oct-2011.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) = ∪ {𝑥 ∈ 𝐴 ∣ 𝜑})
Theorem	nfriota1 5860*	The abstraction variable in a restricted iota descriptor isn't free. (Contributed by NM, 12-Oct-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥(℩𝑥 ∈ 𝐴 𝜑)
Theorem	nfriotadxy 5861*	Deduction version of nfriota 5862. (Contributed by Jim Kingdon, 12-Jan-2019.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜓))
Theorem	nfriota 5862*	A variable not free in a wff remains so in a restricted iota descriptor. (Contributed by NM, 12-Oct-2011.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜑)
Theorem	cbvriota 5863*	Change bound variable in a restricted description binder. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓)
Theorem	cbvriotav 5864*	Change bound variable in a restricted description binder. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓)
Theorem	csbriotag 5865*	Interchange class substitution and restricted description binder. (Contributed by NM, 24-Feb-2013.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(℩𝑦 ∈ 𝐵 𝜑) = (℩𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑))
Theorem	riotacl2 5866	Membership law for "the unique element in 𝐴 such that 𝜑." (Contributed by NM, 21-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})
Theorem	riotacl 5867*	Closure of restricted iota. (Contributed by NM, 21-Aug-2011.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴)
Theorem	riotasbc 5868	Substitution law for descriptions. (Contributed by NM, 23-Aug-2011.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → [(℩𝑥 ∈ 𝐴 𝜑) / 𝑥]𝜑)
Theorem	riotabidva 5869*	Equivalent wff's yield equal restricted class abstractions (deduction form). (rabbidva 2740 analog.) (Contributed by NM, 17-Jan-2012.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒))
Theorem	riotabiia 5870	Equivalent wff's yield equal restricted iotas (inference form). (rabbiia 2737 analog.) (Contributed by NM, 16-Jan-2012.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐴 𝜓)
Theorem	riota1 5871*	Property of restricted iota. Compare iota1 5210. (Contributed by Mario Carneiro, 15-Oct-2016.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝑥))
Theorem	riota1a 5872	Property of iota. (Contributed by NM, 23-Aug-2011.)
⊢ ((𝑥 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜑 ↔ (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) = 𝑥))
Theorem	riota2df 5873*	A deduction version of riota2f 5874. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ ∃!𝑥 ∈ 𝐴 𝜓) → (𝜒 ↔ (℩𝑥 ∈ 𝐴 𝜓) = 𝐵))
Theorem	riota2f 5874*	This theorem shows a condition that allows us to represent a descriptor with a class expression 𝐵. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵))
Theorem	riota2 5875*	This theorem shows a condition that allows us to represent a descriptor with a class expression 𝐵. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 10-Dec-2016.)
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵))
Theorem	riotaprop 5876*	Properties of a restricted definite description operator. Todo (df-riota 5852 update): can some uses of riota2f 5874 be shortened with this? (Contributed by NM, 23-Nov-2013.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐵 = (℩𝑥 ∈ 𝐴 𝜑)    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (𝐵 ∈ 𝐴 ∧ 𝜓))
Theorem	riota5f 5877*	A method for computing restricted iota. (Contributed by NM, 16-Apr-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝑥 = 𝐵))    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = 𝐵)
Theorem	riota5 5878*	A method for computing restricted iota. (Contributed by NM, 20-Oct-2011.) (Revised by Mario Carneiro, 6-Dec-2016.)
⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝑥 = 𝐵))    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = 𝐵)
Theorem	riotass2 5879*	Restriction of a unique element to a smaller class. (Contributed by NM, 21-Aug-2011.) (Revised by NM, 22-Mar-2013.)
⊢ (((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜓)) → (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜓))
Theorem	riotass 5880*	Restriction of a unique element to a smaller class. (Contributed by NM, 19-Oct-2005.) (Revised by Mario Carneiro, 24-Dec-2016.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑) → (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜑))
Theorem	moriotass 5881*	Restriction of a unique element to a smaller class. (Contributed by NM, 19-Feb-2006.) (Revised by NM, 16-Jun-2017.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐵 𝜑) → (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜑))
Theorem	snriota 5882	A restricted class abstraction with a unique member can be expressed as a singleton. (Contributed by NM, 30-May-2006.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {(℩𝑥 ∈ 𝐴 𝜑)})
Theorem	eusvobj2 5883*	Specify the same property in two ways when class 𝐵(𝑦) is single-valued. (Contributed by NM, 1-Nov-2010.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 → (∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∀𝑦 ∈ 𝐴 𝑥 = 𝐵))
Theorem	eusvobj1 5884*	Specify the same object in two ways when class 𝐵(𝑦) is single-valued. (Contributed by NM, 1-Nov-2010.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 → (℩𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵) = (℩𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵))
Theorem	f1ofveu 5885*	There is one domain element for each value of a one-to-one onto function. (Contributed by NM, 26-May-2006.)
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ∃!𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐶)
Theorem	f1ocnvfv3 5886*	Value of the converse of a one-to-one onto function. (Contributed by NM, 26-May-2006.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (◡𝐹‘𝐶) = (℩𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐶))
Theorem	riotaund 5887*	Restricted iota equals the empty set when not meaningful. (Contributed by NM, 16-Jan-2012.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 13-Sep-2018.)
⊢ (¬ ∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) = ∅)
Theorem	acexmidlema 5888*	Lemma for acexmid 5896. (Contributed by Jim Kingdon, 6-Aug-2019.)
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)}    &   ⊢ 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)}    &   ⊢ 𝐶 = {𝐴, 𝐵}    ⇒   ⊢ ({∅} ∈ 𝐴 → 𝜑)
Theorem	acexmidlemb 5889*	Lemma for acexmid 5896. (Contributed by Jim Kingdon, 6-Aug-2019.)
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)}    &   ⊢ 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)}    &   ⊢ 𝐶 = {𝐴, 𝐵}    ⇒   ⊢ (∅ ∈ 𝐵 → 𝜑)
Theorem	acexmidlemph 5890*	Lemma for acexmid 5896. (Contributed by Jim Kingdon, 6-Aug-2019.)
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)}    &   ⊢ 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)}    &   ⊢ 𝐶 = {𝐴, 𝐵}    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	acexmidlemab 5891*	Lemma for acexmid 5896. (Contributed by Jim Kingdon, 6-Aug-2019.)
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)}    &   ⊢ 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)}    &   ⊢ 𝐶 = {𝐴, 𝐵}    ⇒   ⊢ (((℩𝑣 ∈ 𝐴 ∃𝑢 ∈ 𝑦 (𝐴 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)) = ∅ ∧ (℩𝑣 ∈ 𝐵 ∃𝑢 ∈ 𝑦 (𝐵 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)) = {∅}) → ¬ 𝜑)
Theorem	acexmidlemcase 5892*	Lemma for acexmid 5896. Here we divide the proof into cases (based on the disjunction implicit in an unordered pair, not the sort of case elimination which relies on excluded middle). The cases are (1) the choice function evaluated at 𝐴 equals {∅}, (2) the choice function evaluated at 𝐵 equals ∅, and (3) the choice function evaluated at 𝐴 equals ∅ and the choice function evaluated at 𝐵 equals {∅}. Because of the way we represent the choice function 𝑦, the choice function evaluated at 𝐴 is (℩𝑣 ∈ 𝐴∃𝑢 ∈ 𝑦(𝐴 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)) and the choice function evaluated at 𝐵 is (℩𝑣 ∈ 𝐵∃𝑢 ∈ 𝑦(𝐵 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)). Other than the difference in notation these work just as (𝑦‘𝐴) and (𝑦‘𝐵) would if 𝑦 were a function as defined by df-fun 5237. Although it isn't exactly about the division into cases, it is also convenient for this lemma to also include the step that if the choice function evaluated at 𝐴 equals {∅}, then {∅} ∈ 𝐴 and likewise for 𝐵. (Contributed by Jim Kingdon, 7-Aug-2019.)
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)}    &   ⊢ 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)}    &   ⊢ 𝐶 = {𝐴, 𝐵}    ⇒   ⊢ (∀𝑧 ∈ 𝐶 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) → ({∅} ∈ 𝐴 ∨ ∅ ∈ 𝐵 ∨ ((℩𝑣 ∈ 𝐴 ∃𝑢 ∈ 𝑦 (𝐴 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)) = ∅ ∧ (℩𝑣 ∈ 𝐵 ∃𝑢 ∈ 𝑦 (𝐵 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)) = {∅})))
Theorem	acexmidlem1 5893*	Lemma for acexmid 5896. List the cases identified in acexmidlemcase 5892 and hook them up to the lemmas which handle each case. (Contributed by Jim Kingdon, 7-Aug-2019.)
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)}    &   ⊢ 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)}    &   ⊢ 𝐶 = {𝐴, 𝐵}    ⇒   ⊢ (∀𝑧 ∈ 𝐶 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) → (𝜑 ∨ ¬ 𝜑))
Theorem	acexmidlem2 5894*	Lemma for acexmid 5896. This builds on acexmidlem1 5893 by noting that every element of 𝐶 is inhabited. (Note that 𝑦 is not quite a function in the df-fun 5237 sense because it uses ordered pairs as described in opthreg 4573 rather than df-op 3616). The set 𝐴 is also found in onsucelsucexmidlem 4546. (Contributed by Jim Kingdon, 5-Aug-2019.)
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)}    &   ⊢ 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)}    &   ⊢ 𝐶 = {𝐴, 𝐵}    ⇒   ⊢ (∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) → (𝜑 ∨ ¬ 𝜑))
Theorem	acexmidlemv 5895*	Lemma for acexmid 5896. This is acexmid 5896 with additional disjoint variable conditions, most notably between 𝜑 and 𝑥. (Contributed by Jim Kingdon, 6-Aug-2019.)
⊢ ∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)    ⇒   ⊢ (𝜑 ∨ ¬ 𝜑)
Theorem	acexmid 5896*	The axiom of choice implies excluded middle. Theorem 1.3 in [Bauer] p. 483. The statement of the axiom of choice given here is ac2 in the Metamath Proof Explorer (version of 3-Aug-2019). In particular, note that the choice function 𝑦 provides a value when 𝑧 is inhabited (as opposed to nonempty as in some statements of the axiom of choice). Essentially the same proof can also be found at "The axiom of choice implies instances of EM", [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic". Often referred to as Diaconescu's theorem, or Diaconescu-Goodman-Myhill theorem, after Radu Diaconescu who discovered it in 1975 in the framework of topos theory and N. D. Goodman and John Myhill in 1978 in the framework of set theory (although it already appeared as an exercise in Errett Bishop's book Foundations of Constructive Analysis from 1967). For this theorem stated using the df-ac 7236 and df-exmid 4213 syntaxes, see exmidac 7239. (Contributed by Jim Kingdon, 4-Aug-2019.)
⊢ ∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)    ⇒   ⊢ (𝜑 ∨ ¬ 𝜑)
2.6.11  Operations
Syntax	co 5897	Extend class notation to include the value of an operation 𝐹 (such as + ) for two arguments 𝐴 and 𝐵. Note that the syntax is simply three class symbols in a row surrounded by parentheses. Since operation values are the only possible class expressions consisting of three class expressions in a row surrounded by parentheses, the syntax is unambiguous.
class (𝐴𝐹𝐵)
Syntax	coprab 5898	Extend class notation to include class abstraction (class builder) of nested ordered pairs.
class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Syntax	cmpo 5899	Extend the definition of a class to include maps-to notation for defining an operation via a rule.
class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Definition	df-ov 5900	Define the value of an operation. Definition of operation value in [Enderton] p. 79. Note that the syntax is simply three class expressions in a row bracketed by parentheses. There are no restrictions of any kind on what those class expressions may be, although only certain kinds of class expressions - a binary operation 𝐹 and its arguments 𝐴 and 𝐵- will be useful for proving meaningful theorems. For example, if class 𝐹 is the operation + and arguments 𝐴 and 𝐵 are 3 and 2 , the expression ( 3 + 2 ) can be proved to equal 5 . This definition is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e. are not sets); see ovprc1 5933 and ovprc2 5934. On the other hand, we often find uses for this definition when 𝐹 is a proper class. 𝐹 is normally equal to a class of nested ordered pairs of the form defined by df-oprab 5901. (Contributed by NM, 28-Feb-1995.)
⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)