P. 73 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 7201-7300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	isoeq5 7201	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
⊢ (𝐵 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐶)))
Theorem	nfiso 7202	Bound-variable hypothesis builder for an isomorphism. (Contributed by NM, 17-May-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ Ⅎ𝑥𝐻    &   ⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝑆    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
Theorem	isof1o 7203	An isomorphism is a one-to-one onto function. (Contributed by NM, 27-Apr-2004.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵)
Theorem	isof1oidb 7204	A function is a bijection iff it is an isomorphism regarding the identity relation. (Contributed by AV, 9-May-2021.)
⊢ (𝐻:𝐴–1-1-onto→𝐵 ↔ 𝐻 Isom I , I (𝐴, 𝐵))
Theorem	isof1oopb 7205	A function is a bijection iff it is an isomorphism regarding the universal class of ordered pairs as relations. (Contributed by AV, 9-May-2021.)
⊢ (𝐻:𝐴–1-1-onto→𝐵 ↔ 𝐻 Isom (V × V), (V × V)(𝐴, 𝐵))
Theorem	isorel 7206	An isomorphism connects binary relations via its function values. (Contributed by NM, 27-Apr-2004.)
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶𝑅𝐷 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝐷)))
Theorem	soisores 7207*	Express the condition of isomorphism on two strict orders for a function's restriction. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (((𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶) ∧ (𝐹:𝐵⟶𝐶 ∧ 𝐴 ⊆ 𝐵)) → ((𝐹 ↾ 𝐴) Isom 𝑅, 𝑆 (𝐴, (𝐹 “ 𝐴)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐹‘𝑥)𝑆(𝐹‘𝑦))))
Theorem	soisoi 7208*	Infer isomorphism from one direction of an order proof for isomorphisms between strict orders. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵))
Theorem	isoid 7209	Identity law for isomorphism. Proposition 6.30(1) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.)
⊢ ( I ↾ 𝐴) Isom 𝑅, 𝑅 (𝐴, 𝐴)
Theorem	isocnv 7210	Converse law for isomorphism. Proposition 6.30(2) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → ◡𝐻 Isom 𝑆, 𝑅 (𝐵, 𝐴))
Theorem	isocnv2 7211	Converse law for isomorphism. (Contributed by Mario Carneiro, 30-Jan-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom ◡𝑅, ◡𝑆(𝐴, 𝐵))
Theorem	isocnv3 7212	Complementation law for isomorphism. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝐶 = ((𝐴 × 𝐴) ∖ 𝑅)    &   ⊢ 𝐷 = ((𝐵 × 𝐵) ∖ 𝑆)    ⇒   ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝐶, 𝐷 (𝐴, 𝐵))
Theorem	isores2 7213	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 7214	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 7215	Induced isomorphism on a subset. (Contributed by Stefan O'Rear, 5-Nov-2014.)
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐾 ⊆ 𝐴 ∧ 𝑋 = (𝐻 “ 𝐾)) → (𝐻 ↾ 𝐾) Isom 𝑅, 𝑆 (𝐾, 𝑋))
Theorem	isotr 7216	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	isomin 7217	Isomorphisms preserve minimal elements. Note that (◡𝑅 “ {𝐷}) is Takeuti and Zaring's idiom for the initial segment {𝑥 ∣ 𝑥𝑅𝐷}. Proposition 6.31(1) of [TakeutiZaring] p. 33. (Contributed by NM, 19-Apr-2004.)
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐶 ∩ (◡𝑅 “ {𝐷})) = ∅ ↔ ((𝐻 “ 𝐶) ∩ (◡𝑆 “ {(𝐻‘𝐷)})) = ∅))
Theorem	isoini 7218	Isomorphisms preserve initial segments. Proposition 6.31(2) of [TakeutiZaring] p. 33. (Contributed by NM, 20-Apr-2004.)
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐷 ∈ 𝐴) → (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝐷}))) = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝐷)})))
Theorem	isoini2 7219	Isomorphisms are isomorphisms on their initial segments. (Contributed by Mario Carneiro, 29-Mar-2014.)
⊢ 𝐶 = (𝐴 ∩ (◡𝑅 “ {𝑋}))    &   ⊢ 𝐷 = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑋)}))    ⇒   ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → (𝐻 ↾ 𝐶) Isom 𝑅, 𝑆 (𝐶, 𝐷))
Theorem	isofrlem 7220*	Lemma for isofr 7222. (Contributed by NM, 29-Apr-2004.) (Revised by Mario Carneiro, 18-Nov-2014.)
⊢ (𝜑 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵))    &   ⊢ (𝜑 → (𝐻 “ 𝑥) ∈ V)    ⇒   ⊢ (𝜑 → (𝑆 Fr 𝐵 → 𝑅 Fr 𝐴))
Theorem	isoselem 7221*	Lemma for isose 7223. (Contributed by Mario Carneiro, 23-Jun-2015.)
⊢ (𝜑 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵))    &   ⊢ (𝜑 → (𝐻 “ 𝑥) ∈ V)    ⇒   ⊢ (𝜑 → (𝑅 Se 𝐴 → 𝑆 Se 𝐵))
Theorem	isofr 7222	An isomorphism preserves well-foundedness. Proposition 6.32(1) of [TakeutiZaring] p. 33. (Contributed by NM, 30-Apr-2004.) (Revised by Mario Carneiro, 18-Nov-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐵))
Theorem	isose 7223	An isomorphism preserves set-like relations. (Contributed by Mario Carneiro, 23-Jun-2015.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Se 𝐴 ↔ 𝑆 Se 𝐵))
Theorem	isofr2 7224	A weak form of isofr 7222 that does not need Replacement. (Contributed by Mario Carneiro, 18-Nov-2014.)
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐵 ∈ 𝑉) → (𝑆 Fr 𝐵 → 𝑅 Fr 𝐴))
Theorem	isopolem 7225	Lemma for isopo 7226. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑆 Po 𝐵 → 𝑅 Po 𝐴))
Theorem	isopo 7226	An isomorphism preserves the property of being a partial order. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Po 𝐴 ↔ 𝑆 Po 𝐵))
Theorem	isosolem 7227	Lemma for isoso 7228. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑆 Or 𝐵 → 𝑅 Or 𝐴))
Theorem	isoso 7228	An isomorphism preserves the property of being a strict total order. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐵))
Theorem	isowe 7229	An isomorphism preserves the property of being a well-ordering. Proposition 6.32(3) of [TakeutiZaring] p. 33. (Contributed by NM, 30-Apr-2004.) (Revised by Mario Carneiro, 18-Nov-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 We 𝐴 ↔ 𝑆 We 𝐵))
Theorem	isowe2 7230*	A weak form of isowe 7229 that does not need Replacement. (Contributed by Mario Carneiro, 18-Nov-2014.)
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ ∀𝑥(𝐻 “ 𝑥) ∈ V) → (𝑆 We 𝐵 → 𝑅 We 𝐴))
Theorem	f1oiso 7231*	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 7232*	Any one-to-one onto function determines an isomorphism with an induced relation 𝑆. (Contributed by Mario Carneiro, 9-Mar-2013.)
⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (◡𝐻‘𝑥)𝑅(◡𝐻‘𝑦))}    ⇒   ⊢ (𝐻:𝐴–1-1-onto→𝐵 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵))
Theorem	f1owe 7233*	Well-ordering of isomorphic relations. (Contributed by NM, 4-Mar-1997.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥)𝑆(𝐹‘𝑦)}    ⇒   ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝑆 We 𝐵 → 𝑅 We 𝐴))
Theorem	weniso 7234	A set-like well-ordering has no nontrivial automorphisms. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹 = ( I ↾ 𝐴))
Theorem	weisoeq 7235	Thus, there is at most one isomorphism between any two set-like well-ordered classes. Class version of wemoiso 7825. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵))) → 𝐹 = 𝐺)
Theorem	weisoeq2 7236	Thus, there is at most one isomorphism between any two set-like well-ordered classes. Class version of wemoiso2 7826. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ (((𝑆 We 𝐵 ∧ 𝑆 Se 𝐵) ∧ (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵))) → 𝐹 = 𝐺)
Theorem	knatar 7237*	The Knaster-Tarski theorem says that every monotone function over a complete lattice has a (least) fixpoint. Here we specialize this theorem to the case when the lattice is the powerset lattice 𝒫 𝐴. (Contributed by Mario Carneiro, 11-Jun-2015.)
⊢ 𝑋 = ∩ {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹‘𝑧) ⊆ 𝑧}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → (𝑋 ⊆ 𝐴 ∧ (𝐹‘𝑋) = 𝑋))
2.3.17  Cantor's Theorem
Theorem	canth 7238	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. For the equinumerosity version, see canth2 8926. Note that 𝐴 must be a set: this theorem does not hold when 𝐴 is too large to be a set; see ncanth 7239 for a counterexample. (Use nex 1803 if you want the form ¬ ∃𝑓𝑓:𝐴–onto→𝒫 𝐴.) (Contributed by NM, 7-Aug-1994.) (Proof shortened by Mario Carneiro, 7-Jun-2016.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ¬ 𝐹:𝐴–onto→𝒫 𝐴
Theorem	ncanth 7239	Cantor's theorem fails for the universal class (which is not a set but a proper class by vprc 5240). Specifically, the identity function maps the universe onto its power class. Compare canth 7238 that works for sets. This failure comes from a limitation of the collection principle (which is necessary to avoid Russell's paradox ru 3716): 𝒫 V, being a class, cannot contain proper classes, so it is no larger than V, which is why the identity function "succeeds" in being surjective onto 𝒫 V (see pwv 4837). See also the remark in ru 3716 about NF, in which Cantor's theorem fails for sets that are "too large". This theorem gives some intuition behind that failure: in NF the universal class is a set, and it equals its own power set. (Contributed by NM, 29-Jun-2004.) (Proof shortened by BJ, 29-Dec-2023.)
⊢ I :V–onto→𝒫 V
2.3.18  Restricted iota (description binder)
Syntax	crio 7240	Extend class notation with restricted description binder.
class (℩𝑥 ∈ 𝐴 𝜑)
Definition	df-riota 7241	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 6395. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 2-Sep-2018.)
⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	riotaeqdv 7242*	Formula-building deduction for iota. (Contributed by NM, 15-Sep-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐵 𝜓))
Theorem	riotabidv 7243*	Formula-building deduction for restricted iota. (Contributed by NM, 15-Sep-2011.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒))
Theorem	riotaeqbidv 7244*	Equality deduction for restricted universal quantifier. (Contributed by NM, 15-Sep-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐵 𝜒))
Theorem	riotaex 7245	Restricted iota is a set. (Contributed by NM, 15-Sep-2011.)
⊢ (℩𝑥 ∈ 𝐴 𝜓) ∈ V
Theorem	riotav 7246	An iota restricted to the universe is unrestricted. (Contributed by NM, 18-Sep-2011.)
⊢ (℩𝑥 ∈ V 𝜑) = (℩𝑥𝜑)
Theorem	riotauni 7247	Restricted iota in terms of class union. (Contributed by NM, 11-Oct-2011.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) = ∪ {𝑥 ∈ 𝐴 ∣ 𝜑})
Theorem	nfriota1 7248*	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	nfriotadw 7249*	Deduction version of nfriota 7254 with a disjoint variable condition, which contrary to nfriotad 7253 does not require ax-13 2373. (Contributed by NM, 18-Feb-2013.) (Revised by Gino Giotto, 26-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜓))
Theorem	cbvriotaw 7250*	Change bound variable in a restricted description binder. Version of cbvriota 7255 with a disjoint variable condition, which does not require ax-13 2373. (Contributed by NM, 18-Mar-2013.) (Revised by Gino Giotto, 26-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓)
Theorem	cbvriotavw 7251*	Change bound variable in a restricted description binder. Version of cbvriotav 7256 with a disjoint variable condition, which requires fewer axioms . (Contributed by NM, 18-Mar-2013.) (Revised by Gino Giotto, 30-Sep-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓)
Theorem	cbvriotavwOLD 7252*	Obsolete version of cbvriotavw 7251 as of 30-Sep-2024. (Contributed by NM, 18-Mar-2013.) (Revised by Gino Giotto, 26-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓)
Theorem	nfriotad 7253	Deduction version of nfriota 7254. Usage of this theorem is discouraged because it depends on ax-13 2373. Use the weaker nfriotadw 7249 when possible. (Contributed by NM, 18-Feb-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜓))
Theorem	nfriota 7254*	A variable not free in a wff remains so in a restricted iota descriptor. (Contributed by NM, 12-Oct-2011.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜑)
Theorem	cbvriota 7255*	Change bound variable in a restricted description binder. Usage of this theorem is discouraged because it depends on ax-13 2373. Use the weaker cbvriotaw 7250 when possible. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓)
Theorem	cbvriotav 7256*	Change bound variable in a restricted description binder. Usage of this theorem is discouraged because it depends on ax-13 2373. Use the weaker cbvriotavw 7251 when possible. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓)
Theorem	csbriota 7257*	Interchange class substitution and restricted description binder. (Contributed by NM, 24-Feb-2013.) (Revised by NM, 2-Sep-2018.)
⊢ ⦋𝐴 / 𝑥⦌(℩𝑦 ∈ 𝐵 𝜑) = (℩𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)
Theorem	riotacl2 7258	Membership law for "the unique element in 𝐴 such that 𝜑". (Contributed by NM, 21-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})
Theorem	riotacl 7259*	Closure of restricted iota. (Contributed by NM, 21-Aug-2011.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴)
Theorem	riotasbc 7260	Substitution law for descriptions. Compare iotasbc 42044. (Contributed by NM, 23-Aug-2011.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → [(℩𝑥 ∈ 𝐴 𝜑) / 𝑥]𝜑)
Theorem	riotabidva 7261*	Equivalent wff's yield equal restricted class abstractions (deduction form). (rabbidva 3414 analog.) (Contributed by NM, 17-Jan-2012.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒))
Theorem	riotabiia 7262	Equivalent wff's yield equal restricted iotas (inference form). (rabbiia 3408 analog.) (Contributed by NM, 16-Jan-2012.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐴 𝜓)
Theorem	riota1 7263*	Property of restricted iota. Compare iota1 6414. (Contributed by Mario Carneiro, 15-Oct-2016.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝑥))
Theorem	riota1a 7264	Property of iota. (Contributed by NM, 23-Aug-2011.)
⊢ ((𝑥 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜑 ↔ (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) = 𝑥))
Theorem	riota2df 7265*	A deduction version of riota2f 7266. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ ∃!𝑥 ∈ 𝐴 𝜓) → (𝜒 ↔ (℩𝑥 ∈ 𝐴 𝜓) = 𝐵))
Theorem	riota2f 7266*	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 7267*	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	riotaeqimp 7268*	If two restricted iota descriptors for an equality are equal, then the terms of the equality are equal. (Contributed by AV, 6-Dec-2020.)
⊢ 𝐼 = (℩𝑎 ∈ 𝑉 𝑋 = 𝐴)    &   ⊢ 𝐽 = (℩𝑎 ∈ 𝑉 𝑌 = 𝐴)    &   ⊢ (𝜑 → ∃!𝑎 ∈ 𝑉 𝑋 = 𝐴)    &   ⊢ (𝜑 → ∃!𝑎 ∈ 𝑉 𝑌 = 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝐼 = 𝐽) → 𝑋 = 𝑌)
Theorem	riotaprop 7269*	Properties of a restricted definite description operator. (Contributed by NM, 23-Nov-2013.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐵 = (℩𝑥 ∈ 𝐴 𝜑)    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (𝐵 ∈ 𝐴 ∧ 𝜓))
Theorem	riota5f 7270*	A method for computing restricted iota. (Contributed by NM, 16-Apr-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝑥 = 𝐵))    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = 𝐵)
Theorem	riota5 7271*	A method for computing restricted iota. (Contributed by NM, 20-Oct-2011.) (Revised by Mario Carneiro, 6-Dec-2016.)
⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝑥 = 𝐵))    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = 𝐵)
Theorem	riotass2 7272*	Restriction of a unique element to a smaller class. (Contributed by NM, 21-Aug-2011.) (Revised by NM, 22-Mar-2013.)
⊢ (((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜓)) → (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜓))
Theorem	riotass 7273*	Restriction of a unique element to a smaller class. (Contributed by NM, 19-Oct-2005.) (Revised by Mario Carneiro, 24-Dec-2016.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑) → (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜑))
Theorem	moriotass 7274*	Restriction of a unique element to a smaller class. (Contributed by NM, 19-Feb-2006.) (Revised by NM, 16-Jun-2017.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐵 𝜑) → (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜑))
Theorem	snriota 7275	A restricted class abstraction with a unique member can be expressed as a singleton. (Contributed by NM, 30-May-2006.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {(℩𝑥 ∈ 𝐴 𝜑)})
Theorem	riotaxfrd 7276*	Change the variable 𝑥 in the expression for "the unique 𝑥 such that 𝜓 " to another variable 𝑦 contained in expression 𝐵. Use reuhypd 5343 to eliminate the last hypothesis. (Contributed by NM, 16-Jan-2012.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑦𝐶    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐵 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ (℩𝑦 ∈ 𝐴 𝜒) ∈ 𝐴) → 𝐶 ∈ 𝐴)    &   ⊢ (𝑥 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑦 = (℩𝑦 ∈ 𝐴 𝜒) → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃!𝑦 ∈ 𝐴 𝑥 = 𝐵)    ⇒   ⊢ ((𝜑 ∧ ∃!𝑥 ∈ 𝐴 𝜓) → (℩𝑥 ∈ 𝐴 𝜓) = 𝐶)
Theorem	eusvobj2 7277*	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 7278*	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 7279*	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 7280*	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 7281*	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	riotassuni 7282*	The restricted iota class is limited in size by the base set. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (℩𝑥 ∈ 𝐴 𝜑) ⊆ (𝒫 ∪ 𝐴 ∪ ∪ 𝐴)
Theorem	riotaclb 7283*	Bidirectional closure of restricted iota when domain is not empty. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 24-Dec-2016.) (Revised by NM, 13-Sep-2018.)
⊢ (¬ ∅ ∈ 𝐴 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴))
2.3.19  Operations
Syntax	co 7284	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. (For an example of how syntax could become ambiguous if we are not careful, see the comment in cneg 11215.)
class (𝐴𝐹𝐵)
Syntax	coprab 7285	Extend class notation to include class abstraction (class builder) of nested ordered pairs.
class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Syntax	cmpo 7286	Extend the definition of a class to include maps-to notation for defining an operation via a rule.
class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Definition	df-ov 7287	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 (see 3p2e5 12133). This definition is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e. are not sets); see ovprc1 7323 and ovprc2 7324. On the other hand, we often find uses for this definition when 𝐹 is a proper class, such as +o in oav 8350. 𝐹 is normally equal to a class of nested ordered pairs of the form defined by df-oprab 7288. (Contributed by NM, 28-Feb-1995.)
⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
Definition	df-oprab 7288*	Define the class abstraction (class builder) of a collection of nested ordered pairs (for use in defining operations). This is a special case of Definition 4.16 of [TakeutiZaring] p. 14. Normally 𝑥, 𝑦, and 𝑧 are distinct, although the definition doesn't strictly require it. See df-ov 7287 for the value of an operation. The brace notation is called "class abstraction" by Quine; it is also called a "class builder" in the literature. The value of an operation given by a class abstraction is given by ovmpo 7442. (Contributed by NM, 12-Mar-1995.)
⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
Definition	df-mpo 7289*	Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from 𝑥, 𝑦 (in 𝐴 × 𝐵) to 𝐶(𝑥, 𝑦)". An extension of df-mpt 5159 for two arguments. (Contributed by NM, 17-Feb-2008.)
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
Theorem	oveq 7290	Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
⊢ (𝐹 = 𝐺 → (𝐴𝐹𝐵) = (𝐴𝐺𝐵))
Theorem	oveq1 7291	Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
Theorem	oveq2 7292	Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
Theorem	oveq12 7293	Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Theorem	oveq1i 7294	Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐶)
Theorem	oveq2i 7295	Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶𝐹𝐴) = (𝐶𝐹𝐵)
Theorem	oveq12i 7296	Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐷)
Theorem	oveqi 7297	Equality inference for operation value. (Contributed by NM, 24-Nov-2007.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶𝐴𝐷) = (𝐶𝐵𝐷)
Theorem	oveq123i 7298	Equality inference for operation value. (Contributed by FL, 11-Jul-2010.)
⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    &   ⊢ 𝐹 = 𝐺    ⇒   ⊢ (𝐴𝐹𝐵) = (𝐶𝐺𝐷)
Theorem	oveq1d 7299	Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
Theorem	oveq2d 7300	Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))