P. 74 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 7301-7400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fliftfund 7301*	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 7302*	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 7303*	The domain and range of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (Fun 𝐹 ↔ 𝐹:ran (𝑥 ∈ 𝑋 ↦ 𝐴)⟶𝑆))
Theorem	fliftval 7304*	The value of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆)    &   ⊢ (𝑥 = 𝑌 → 𝐴 = 𝐶)    &   ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷)    &   ⊢ (𝜑 → Fun 𝐹)    ⇒   ⊢ ((𝜑 ∧ 𝑌 ∈ 𝑋) → (𝐹‘𝐶) = 𝐷)
Theorem	isoeq1 7305	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
⊢ (𝐻 = 𝐺 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵)))
Theorem	isoeq2 7306	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
⊢ (𝑅 = 𝑇 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑇, 𝑆 (𝐴, 𝐵)))
Theorem	isoeq3 7307	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
⊢ (𝑆 = 𝑇 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑇 (𝐴, 𝐵)))
Theorem	isoeq4 7308	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
⊢ (𝐴 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐶, 𝐵)))
Theorem	isoeq5 7309	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
⊢ (𝐵 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐶)))
Theorem	nfiso 7310	Bound-variable hypothesis builder for an isomorphism. (Contributed by NM, 17-May-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ Ⅎ𝑥𝐻    &   ⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝑆    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
Theorem	isof1o 7311	An isomorphism is a one-to-one onto function. (Contributed by NM, 27-Apr-2004.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵)
Theorem	isof1oidb 7312	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 7313	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 7314	An isomorphism connects binary relations via its function values. (Contributed by NM, 27-Apr-2004.)
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶𝑅𝐷 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝐷)))
Theorem	soisores 7315*	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 7316*	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 7317	Identity law for isomorphism. Proposition 6.30(1) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.)
⊢ ( I ↾ 𝐴) Isom 𝑅, 𝑅 (𝐴, 𝐴)
Theorem	isocnv 7318	Converse law for isomorphism. Proposition 6.30(2) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → ◡𝐻 Isom 𝑆, 𝑅 (𝐵, 𝐴))
Theorem	isocnv2 7319	Converse law for isomorphism. (Contributed by Mario Carneiro, 30-Jan-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom ◡𝑅, ◡𝑆(𝐴, 𝐵))
Theorem	isocnv3 7320	Complementation law for isomorphism. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝐶 = ((𝐴 × 𝐴) ∖ 𝑅)    &   ⊢ 𝐷 = ((𝐵 × 𝐵) ∖ 𝑆)    ⇒   ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝐶, 𝐷 (𝐴, 𝐵))
Theorem	isores2 7321	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 7322	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 7323	Induced isomorphism on a subset. (Contributed by Stefan O'Rear, 5-Nov-2014.)
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐾 ⊆ 𝐴 ∧ 𝑋 = (𝐻 “ 𝐾)) → (𝐻 ↾ 𝐾) Isom 𝑅, 𝑆 (𝐾, 𝑋))
Theorem	isotr 7324	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 7325	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 7326	Isomorphisms preserve initial segments. Proposition 6.31(2) of [TakeutiZaring] p. 33. (Contributed by NM, 20-Apr-2004.)
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐷 ∈ 𝐴) → (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝐷}))) = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝐷)})))
Theorem	isoini2 7327	Isomorphisms are isomorphisms on their initial segments. (Contributed by Mario Carneiro, 29-Mar-2014.)
⊢ 𝐶 = (𝐴 ∩ (◡𝑅 “ {𝑋}))    &   ⊢ 𝐷 = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑋)}))    ⇒   ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → (𝐻 ↾ 𝐶) Isom 𝑅, 𝑆 (𝐶, 𝐷))
Theorem	isofrlem 7328*	Lemma for isofr 7330. (Contributed by NM, 29-Apr-2004.) (Revised by Mario Carneiro, 18-Nov-2014.)
⊢ (𝜑 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵))    &   ⊢ (𝜑 → (𝐻 “ 𝑥) ∈ V)    ⇒   ⊢ (𝜑 → (𝑆 Fr 𝐵 → 𝑅 Fr 𝐴))
Theorem	isoselem 7329*	Lemma for isose 7331. (Contributed by Mario Carneiro, 23-Jun-2015.)
⊢ (𝜑 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵))    &   ⊢ (𝜑 → (𝐻 “ 𝑥) ∈ V)    ⇒   ⊢ (𝜑 → (𝑅 Se 𝐴 → 𝑆 Se 𝐵))
Theorem	isofr 7330	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 7331	An isomorphism preserves set-like relations. (Contributed by Mario Carneiro, 23-Jun-2015.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Se 𝐴 ↔ 𝑆 Se 𝐵))
Theorem	isofr2 7332	A weak form of isofr 7330 that does not need Replacement. (Contributed by Mario Carneiro, 18-Nov-2014.)
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐵 ∈ 𝑉) → (𝑆 Fr 𝐵 → 𝑅 Fr 𝐴))
Theorem	isopolem 7333	Lemma for isopo 7334. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑆 Po 𝐵 → 𝑅 Po 𝐴))
Theorem	isopo 7334	An isomorphism preserves the property of being a partial order. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Po 𝐴 ↔ 𝑆 Po 𝐵))
Theorem	isosolem 7335	Lemma for isoso 7336. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑆 Or 𝐵 → 𝑅 Or 𝐴))
Theorem	isoso 7336	An isomorphism preserves the property of being a strict total order. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐵))
Theorem	isowe 7337	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 7338*	A weak form of isowe 7337 that does not need Replacement. (Contributed by Mario Carneiro, 18-Nov-2014.)
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ ∀𝑥(𝐻 “ 𝑥) ∈ V) → (𝑆 We 𝐵 → 𝑅 We 𝐴))
Theorem	f1oiso 7339*	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 7340*	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 7341*	Well-ordering of isomorphic relations. (Contributed by NM, 4-Mar-1997.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥)𝑆(𝐹‘𝑦)}    ⇒   ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝑆 We 𝐵 → 𝑅 We 𝐴))
Theorem	weniso 7342	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 7343	Thus, there is at most one isomorphism between any two set-like well-ordered classes. Class version of wemoiso 7958. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵))) → 𝐹 = 𝐺)
Theorem	weisoeq2 7344	Thus, there is at most one isomorphism between any two set-like well-ordered classes. Class version of wemoiso2 7959. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ (((𝑆 We 𝐵 ∧ 𝑆 Se 𝐵) ∧ (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵))) → 𝐹 = 𝐺)
Theorem	knatar 7345*	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.)
⊢ 𝑋 = ∩ {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹‘𝑧) ⊆ 𝑧}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → (𝑋 ⊆ 𝐴 ∧ (𝐹‘𝑋) = 𝑋))
Theorem	fvresval 7346	The value of a restricted function at a class is either the empty set or the value of the unrestricted function at that class. (Contributed by Scott Fenton, 4-Sep-2011.)
⊢ (((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴) ∨ ((𝐹 ↾ 𝐵)‘𝐴) = ∅)
Theorem	funeldmb 7347	If ∅ is not part of the range of a function 𝐹, then 𝐴 is in the domain of 𝐹 iff (𝐹‘𝐴) ≠ ∅. (Contributed by Scott Fenton, 7-Dec-2021.)
⊢ ((Fun 𝐹 ∧ ¬ ∅ ∈ ran 𝐹) → (𝐴 ∈ dom 𝐹 ↔ (𝐹‘𝐴) ≠ ∅))
Theorem	eqfunresadj 7348	Law for adjoining an element to restrictions of functions. (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (𝐹 ↾ 𝑋) = (𝐺 ↾ 𝑋) ∧ (𝑌 ∈ dom 𝐹 ∧ 𝑌 ∈ dom 𝐺 ∧ (𝐹‘𝑌) = (𝐺‘𝑌))) → (𝐹 ↾ (𝑋 ∪ {𝑌})) = (𝐺 ↾ (𝑋 ∪ {𝑌})))
Theorem	eqfunressuc 7349	Law for equality of restriction to successors. This is primarily useful when 𝑋 is an ordinal, but it does not require that. (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (𝐹 ↾ 𝑋) = (𝐺 ↾ 𝑋) ∧ (𝑋 ∈ dom 𝐹 ∧ 𝑋 ∈ dom 𝐺 ∧ (𝐹‘𝑋) = (𝐺‘𝑋))) → (𝐹 ↾ suc 𝑋) = (𝐺 ↾ suc 𝑋))
Theorem	fnssintima 7350*	Condition for subset of an intersection of an image. (Contributed by Scott Fenton, 16-Aug-2024.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ⊆ ∩ (𝐹 “ 𝐵) ↔ ∀𝑥 ∈ 𝐵 𝐶 ⊆ (𝐹‘𝑥)))
Theorem	imaeqsexvOLD 7351*	Obsolete version of rexima 7226 as of 14-Aug-2025. Duplicate version of rexima 7226. (Contributed by Scott Fenton, 27-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∃𝑥 ∈ (𝐹 “ 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓))
Theorem	imaeqsalvOLD 7352*	Obsolete version of ralima 7225 as of 14-Aug-2025. Duplicate version of ralima 7225. (Contributed by Scott Fenton, 27-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∀𝑥 ∈ (𝐹 “ 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓))
Theorem	fnimasnd 7353	The image of a function by a singleton whose element is in the domain of the function. (Contributed by Steven Nguyen, 7-Jun-2023.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝐹 “ {𝑆}) = {(𝐹‘𝑆)})
2.3.17  Cantor's Theorem
Theorem	canth 7354	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 9106. Note that 𝐴 must be a set: this theorem does not hold when 𝐴 is too large to be a set; see ncanth 7355 for a counterexample. (Use nex 1823 if you want the form ¬ ∃𝑓𝑓:𝐴–onto→𝒫 𝐴.) (Contributed by NM, 7-Aug-1994.) (Proof shortened by Mario Carneiro, 7-Jun-2016.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ¬ 𝐹:𝐴–onto→𝒫 𝐴
Theorem	ncanth 7355	Cantor's theorem fails for the universal class (which is not a set but a proper class by vprc 5275). Specifically, the identity function maps the universe onto its power class. Compare canth 7354 that works for sets. This failure comes from a limitation of the collection principle (which is necessary to avoid Russell's paradox ru 3746): 𝒫 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 4865). See also the remark in ru 3746 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 7356	Extend class notation with restricted description binder.
class (℩𝑥 ∈ 𝐴 𝜑)
Definition	df-riota 7357	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 6481. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 2-Sep-2018.)
⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	riotaeqdv 7358*	Formula-building deduction for iota. (Contributed by NM, 15-Sep-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐵 𝜓))
Theorem	riotabidv 7359*	Formula-building deduction for restricted iota. (Contributed by NM, 15-Sep-2011.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒))
Theorem	riotaeqbidv 7360*	Equality deduction for restricted universal quantifier. (Contributed by NM, 15-Sep-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐵 𝜒))
Theorem	riotaex 7361	Restricted iota is a set. (Contributed by NM, 15-Sep-2011.)
⊢ (℩𝑥 ∈ 𝐴 𝜓) ∈ V
Theorem	riotav 7362	An iota restricted to the universe is unrestricted. (Contributed by NM, 18-Sep-2011.)
⊢ (℩𝑥 ∈ V 𝜑) = (℩𝑥𝜑)
Theorem	riotauni 7363	Restricted iota in terms of class union. (Contributed by NM, 11-Oct-2011.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) = ∪ {𝑥 ∈ 𝐴 ∣ 𝜑})
Theorem	nfriota1 7364*	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 7365*	Deduction version of nfriota 7369 with a disjoint variable condition, which contrary to nfriotad 7368 does not require ax-13 2406. (Contributed by NM, 18-Feb-2013.) Avoid ax-13 2406. (Revised by GG, 26-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜓))
Theorem	cbvriotaw 7366*	Change bound variable in a restricted description binder. Version of cbvriota 7370 with a disjoint variable condition, which does not require ax-13 2406. (Contributed by NM, 18-Mar-2013.) Avoid ax-13 2406. (Revised by GG, 26-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓)
Theorem	cbvriotavw 7367*	Change bound variable in a restricted description binder. Version of cbvriotav 7371 with a disjoint variable condition, which requires fewer axioms . (Contributed by NM, 18-Mar-2013.) (Revised by GG, 30-Sep-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓)
Theorem	nfriotad 7368	Deduction version of nfriota 7369. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker nfriotadw 7365 when possible. (Contributed by NM, 18-Feb-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜓))
Theorem	nfriota 7369*	A variable not free in a wff remains so in a restricted iota descriptor. (Contributed by NM, 12-Oct-2011.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜑)
Theorem	cbvriota 7370*	Change bound variable in a restricted description binder. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker cbvriotaw 7366 when possible. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓)
Theorem	cbvriotav 7371*	Change bound variable in a restricted description binder. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker cbvriotavw 7367 when possible. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓)
Theorem	csbriota 7372*	Interchange class substitution and restricted description binder. (Contributed by NM, 24-Feb-2013.) (Revised by NM, 2-Sep-2018.)
⊢ ⦋𝐴 / 𝑥⦌(℩𝑦 ∈ 𝐵 𝜑) = (℩𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)
Theorem	riotacl2 7373	Membership law for "the unique element in 𝐴 such that 𝜑". (Contributed by NM, 21-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})
Theorem	riotacl 7374*	Closure of restricted iota. (Contributed by NM, 21-Aug-2011.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴)
Theorem	riotasbc 7375	Substitution law for descriptions. Compare iotasbc 44993. (Contributed by NM, 23-Aug-2011.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → [(℩𝑥 ∈ 𝐴 𝜑) / 𝑥]𝜑)
Theorem	riotabidva 7376*	Equivalent wff's yield equal restricted class abstractions (deduction form). (rabbidva 3423 analog.) (Contributed by NM, 17-Jan-2012.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒))
Theorem	riotabiia 7377	Equivalent wff's yield equal restricted iotas (inference form). (rabbiia 3421 analog.) (Contributed by NM, 16-Jan-2012.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐴 𝜓)
Theorem	riota1 7378*	Property of restricted iota. Compare iota1 6504. (Contributed by Mario Carneiro, 15-Oct-2016.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝑥))
Theorem	riota1a 7379	Property of iota. (Contributed by NM, 23-Aug-2011.)
⊢ ((𝑥 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜑 ↔ (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) = 𝑥))
Theorem	riota2df 7380*	A deduction version of riota2f 7381. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ ∃!𝑥 ∈ 𝐴 𝜓) → (𝜒 ↔ (℩𝑥 ∈ 𝐴 𝜓) = 𝐵))
Theorem	riota2f 7381*	This theorem shows a condition that allows to represent a descriptor with a class expression 𝐵. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵))
Theorem	riota2 7382*	This theorem shows a condition that allows to represent a descriptor with a class expression 𝐵. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 10-Dec-2016.)
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵))
Theorem	riotaeqimp 7383*	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 7384*	Properties of a restricted definite description operator. (Contributed by NM, 23-Nov-2013.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐵 = (℩𝑥 ∈ 𝐴 𝜑)    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (𝐵 ∈ 𝐴 ∧ 𝜓))
Theorem	riota5f 7385*	A method for computing restricted iota. (Contributed by NM, 16-Apr-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝑥 = 𝐵))    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = 𝐵)
Theorem	riota5 7386*	A method for computing restricted iota. (Contributed by NM, 20-Oct-2011.) (Revised by Mario Carneiro, 6-Dec-2016.)
⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝑥 = 𝐵))    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = 𝐵)
Theorem	riotass2 7387*	Restriction of a unique element to a smaller class. (Contributed by NM, 21-Aug-2011.) (Revised by NM, 22-Mar-2013.)
⊢ (((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜓)) → (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜓))
Theorem	riotass 7388*	Restriction of a unique element to a smaller class. (Contributed by NM, 19-Oct-2005.) (Revised by Mario Carneiro, 24-Dec-2016.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑) → (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜑))
Theorem	moriotass 7389*	Restriction of a unique element to a smaller class. (Contributed by NM, 19-Feb-2006.) (Revised by NM, 16-Jun-2017.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐵 𝜑) → (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜑))
Theorem	snriota 7390	A restricted class abstraction with a unique member can be expressed as a singleton. (Contributed by NM, 30-May-2006.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {(℩𝑥 ∈ 𝐴 𝜑)})
Theorem	riotaxfrd 7391*	Change the variable 𝑥 in the expression for "the unique 𝑥 such that 𝜓 " to another variable 𝑦 contained in expression 𝐵. Use reuhypd 5381 to eliminate the last hypothesis. (Contributed by NM, 16-Jan-2012.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑦𝐶    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐵 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ (℩𝑦 ∈ 𝐴 𝜒) ∈ 𝐴) → 𝐶 ∈ 𝐴)    &   ⊢ (𝑥 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑦 = (℩𝑦 ∈ 𝐴 𝜒) → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃!𝑦 ∈ 𝐴 𝑥 = 𝐵)    ⇒   ⊢ ((𝜑 ∧ ∃!𝑥 ∈ 𝐴 𝜓) → (℩𝑥 ∈ 𝐴 𝜓) = 𝐶)
Theorem	eusvobj2 7392*	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 7393*	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 7394*	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 7395*	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 7396*	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 7397*	The restricted iota class is limited in size by the base set. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (℩𝑥 ∈ 𝐴 𝜑) ⊆ (𝒫 ∪ 𝐴 ∪ ∪ 𝐴)
Theorem	riotaclb 7398*	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.)
⊢ (¬ ∅ ∈ 𝐴 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴))
Theorem	riotarab 7399*	Restricted iota of a restricted abstraction. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜓}𝜒) = (℩𝑥 ∈ 𝐴 (𝜑 ∧ 𝜒))
2.3.19  Operations
Syntax	co 7400	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 11430.)
class (𝐴𝐹𝐵)