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	fcof1o 7301	Show that two functions are inverse to each other by computing their compositions. (Contributed by Mario Carneiro, 21-Mar-2015.) (Proof shortened by AV, 15-Dec-2019.)
⊢ (((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ((𝐹 ∘ 𝐺) = ( I ↾ 𝐵) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐴))) → (𝐹:𝐴–1-1-onto→𝐵 ∧ ◡𝐹 = 𝐺))
Theorem	2fvcoidd 7302*	Show that the composition of two functions is the identity function by applying both functions to each value of the domain of the first function. (Contributed by AV, 15-Dec-2019.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)    &   ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 (𝐺‘(𝐹‘𝑎)) = 𝑎)    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) = ( I ↾ 𝐴))
Theorem	2fvidf1od 7303*	A function is bijective if it has an inverse function. (Contributed by AV, 15-Dec-2019.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)    &   ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 (𝐺‘(𝐹‘𝑎)) = 𝑎)    &   ⊢ (𝜑 → ∀𝑏 ∈ 𝐵 (𝐹‘(𝐺‘𝑏)) = 𝑏)    ⇒   ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵)
Theorem	2fvidinvd 7304*	Show that two functions are inverse to each other by applying them twice to each value of their domains. (Contributed by AV, 13-Dec-2019.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)    &   ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 (𝐺‘(𝐹‘𝑎)) = 𝑎)    &   ⊢ (𝜑 → ∀𝑏 ∈ 𝐵 (𝐹‘(𝐺‘𝑏)) = 𝑏)    ⇒   ⊢ (𝜑 → ◡𝐹 = 𝐺)
Theorem	foeqcnvco 7305	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 7306	Condition for function equality in terms of vanishing of the composition with the inverse. (Contributed by Stefan O'Rear, 12-Feb-2015.) (Proof shortened by Wolf Lammen, 29-May-2024.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → (𝐹 = 𝐺 ↔ (◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴)))
Theorem	fveqf1o 7307	Given a bijection 𝐹, produce another bijection 𝐺 which additionally maps two specified points. (Contributed by Mario Carneiro, 30-May-2015.)
⊢ 𝐺 = (𝐹 ∘ (( I ↾ (𝐴 ∖ {𝐶, (◡𝐹‘𝐷)})) ∪ {⟨𝐶, (◡𝐹‘𝐷)⟩, ⟨(◡𝐹‘𝐷), 𝐶⟩}))    ⇒   ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐺:𝐴–1-1-onto→𝐵 ∧ (𝐺‘𝐶) = 𝐷))
Theorem	f1ocoima 7308	The composition of two bijections as bijection onto the image of the range of the first bijection. (Contributed by AV, 15-Aug-2025.)
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐵 ⊆ 𝐶) → (𝐺 ∘ 𝐹):𝐴–1-1-onto→(𝐺 “ 𝐵))
Theorem	nf1const 7309	A constant function from at least two elements is not one-to-one. (Contributed by AV, 30-Mar-2024.)
⊢ ((𝐹:𝐴⟶{𝐵} ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌)) → ¬ 𝐹:𝐴–1-1→𝐶)
Theorem	nf1oconst 7310	A constant function from at least two elements is not bijective. (Contributed by AV, 30-Mar-2024.)
⊢ ((𝐹:𝐴⟶{𝐵} ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌)) → ¬ 𝐹:𝐴–1-1-onto→𝐶)
Theorem	f1ofvswap 7311	Swapping two values in a bijection between two classes yields another bijection between those classes. (Contributed by BTernaryTau, 31-Aug-2024.)
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝐹 ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {⟨𝑋, (𝐹‘𝑌)⟩, ⟨𝑌, (𝐹‘𝑋)⟩}):𝐴–1-1-onto→𝐵)
Theorem	fvf1pr 7312	Values of a one-to-one function between two sets with two elements. Actually, such a function is a bijection. (Contributed by AV, 22-Jul-2025.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ 𝐹:{𝐴, 𝐵}–1-1→{𝑋, 𝑌}) → (((𝐹‘𝐴) = 𝑋 ∧ (𝐹‘𝐵) = 𝑌) ∨ ((𝐹‘𝐴) = 𝑌 ∧ (𝐹‘𝐵) = 𝑋)))
Theorem	fliftrel 7313*	𝐹, a function lift, is a subset of 𝑅 × 𝑆. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝐹 ⊆ (𝑅 × 𝑆))
Theorem	fliftel 7314*	Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐶𝐹𝐷 ↔ ∃𝑥 ∈ 𝑋 (𝐶 = 𝐴 ∧ 𝐷 = 𝐵)))
Theorem	fliftel1 7315*	Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴𝐹𝐵)
Theorem	fliftcnv 7316*	Converse of the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ◡𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐵, 𝐴⟩))
Theorem	fliftfun 7317*	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 7318*	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 7319*	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 7320*	The domain and range of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (Fun 𝐹 ↔ 𝐹:ran (𝑥 ∈ 𝑋 ↦ 𝐴)⟶𝑆))
Theorem	fliftval 7321*	The value of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆)    &   ⊢ (𝑥 = 𝑌 → 𝐴 = 𝐶)    &   ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷)    &   ⊢ (𝜑 → Fun 𝐹)    ⇒   ⊢ ((𝜑 ∧ 𝑌 ∈ 𝑋) → (𝐹‘𝐶) = 𝐷)
Theorem	isoeq1 7322	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
⊢ (𝐻 = 𝐺 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵)))
Theorem	isoeq2 7323	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
⊢ (𝑅 = 𝑇 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑇, 𝑆 (𝐴, 𝐵)))
Theorem	isoeq3 7324	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
⊢ (𝑆 = 𝑇 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑇 (𝐴, 𝐵)))
Theorem	isoeq4 7325	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
⊢ (𝐴 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐶, 𝐵)))
Theorem	isoeq5 7326	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
⊢ (𝐵 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐶)))
Theorem	nfiso 7327	Bound-variable hypothesis builder for an isomorphism. (Contributed by NM, 17-May-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ Ⅎ𝑥𝐻    &   ⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝑆    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
Theorem	isof1o 7328	An isomorphism is a one-to-one onto function. (Contributed by NM, 27-Apr-2004.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵)
Theorem	isof1oidb 7329	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 7330	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 7331	An isomorphism connects binary relations via its function values. (Contributed by NM, 27-Apr-2004.)
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶𝑅𝐷 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝐷)))
Theorem	soisores 7332*	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 7333*	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 7334	Identity law for isomorphism. Proposition 6.30(1) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.)
⊢ ( I ↾ 𝐴) Isom 𝑅, 𝑅 (𝐴, 𝐴)
Theorem	isocnv 7335	Converse law for isomorphism. Proposition 6.30(2) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → ◡𝐻 Isom 𝑆, 𝑅 (𝐵, 𝐴))
Theorem	isocnv2 7336	Converse law for isomorphism. (Contributed by Mario Carneiro, 30-Jan-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom ◡𝑅, ◡𝑆(𝐴, 𝐵))
Theorem	isocnv3 7337	Complementation law for isomorphism. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝐶 = ((𝐴 × 𝐴) ∖ 𝑅)    &   ⊢ 𝐷 = ((𝐵 × 𝐵) ∖ 𝑆)    ⇒   ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝐶, 𝐷 (𝐴, 𝐵))
Theorem	isores2 7338	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 7339	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 7340	Induced isomorphism on a subset. (Contributed by Stefan O'Rear, 5-Nov-2014.)
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐾 ⊆ 𝐴 ∧ 𝑋 = (𝐻 “ 𝐾)) → (𝐻 ↾ 𝐾) Isom 𝑅, 𝑆 (𝐾, 𝑋))
Theorem	isotr 7341	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 7342	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 7343	Isomorphisms preserve initial segments. Proposition 6.31(2) of [TakeutiZaring] p. 33. (Contributed by NM, 20-Apr-2004.)
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐷 ∈ 𝐴) → (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝐷}))) = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝐷)})))
Theorem	isoini2 7344	Isomorphisms are isomorphisms on their initial segments. (Contributed by Mario Carneiro, 29-Mar-2014.)
⊢ 𝐶 = (𝐴 ∩ (◡𝑅 “ {𝑋}))    &   ⊢ 𝐷 = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑋)}))    ⇒   ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → (𝐻 ↾ 𝐶) Isom 𝑅, 𝑆 (𝐶, 𝐷))
Theorem	isofrlem 7345*	Lemma for isofr 7347. (Contributed by NM, 29-Apr-2004.) (Revised by Mario Carneiro, 18-Nov-2014.)
⊢ (𝜑 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵))    &   ⊢ (𝜑 → (𝐻 “ 𝑥) ∈ V)    ⇒   ⊢ (𝜑 → (𝑆 Fr 𝐵 → 𝑅 Fr 𝐴))
Theorem	isoselem 7346*	Lemma for isose 7348. (Contributed by Mario Carneiro, 23-Jun-2015.)
⊢ (𝜑 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵))    &   ⊢ (𝜑 → (𝐻 “ 𝑥) ∈ V)    ⇒   ⊢ (𝜑 → (𝑅 Se 𝐴 → 𝑆 Se 𝐵))
Theorem	isofr 7347	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 7348	An isomorphism preserves set-like relations. (Contributed by Mario Carneiro, 23-Jun-2015.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Se 𝐴 ↔ 𝑆 Se 𝐵))
Theorem	isofr2 7349	A weak form of isofr 7347 that does not need Replacement. (Contributed by Mario Carneiro, 18-Nov-2014.)
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐵 ∈ 𝑉) → (𝑆 Fr 𝐵 → 𝑅 Fr 𝐴))
Theorem	isopolem 7350	Lemma for isopo 7351. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑆 Po 𝐵 → 𝑅 Po 𝐴))
Theorem	isopo 7351	An isomorphism preserves the property of being a partial order. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Po 𝐴 ↔ 𝑆 Po 𝐵))
Theorem	isosolem 7352	Lemma for isoso 7353. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑆 Or 𝐵 → 𝑅 Or 𝐴))
Theorem	isoso 7353	An isomorphism preserves the property of being a strict total order. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐵))
Theorem	isowe 7354	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 7355*	A weak form of isowe 7354 that does not need Replacement. (Contributed by Mario Carneiro, 18-Nov-2014.)
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ ∀𝑥(𝐻 “ 𝑥) ∈ V) → (𝑆 We 𝐵 → 𝑅 We 𝐴))
Theorem	f1oiso 7356*	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 7357*	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 7358*	Well-ordering of isomorphic relations. (Contributed by NM, 4-Mar-1997.) Strengthen to biconditional. (Revised by Eric Schmidt, 5-Aug-2026.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥)𝑆(𝐹‘𝑦)}    ⇒   ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝑅 We 𝐴 ↔ 𝑆 We 𝐵))
Theorem	f1oweOLD 7359*	Obsolete version of f1owe as of 5-Aug-2026. (Contributed by NM, 4-Mar-1997.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥)𝑆(𝐹‘𝑦)}    ⇒   ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝑆 We 𝐵 → 𝑅 We 𝐴))
Theorem	f1we 7360*	Pull back a well ordering by a one-to-one function. (Contributed by Eric Schmidt, 4-Aug-2026.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥)𝑆(𝐹‘𝑦)}    ⇒   ⊢ (𝐹:𝐴–1-1→𝐵 → (𝑆 We 𝐵 → 𝑅 We 𝐴))
Theorem	weniso 7361	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 7362	Thus, there is at most one isomorphism between any two set-like well-ordered classes. Class version of wemoiso 7974. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵))) → 𝐹 = 𝐺)
Theorem	weisoeq2 7363	Thus, there is at most one isomorphism between any two set-like well-ordered classes. Class version of wemoiso2 7975. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ (((𝑆 We 𝐵 ∧ 𝑆 Se 𝐵) ∧ (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵))) → 𝐹 = 𝐺)
Theorem	knatar 7364*	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 7365	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 7366	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 7367	Law for adjoining an element to restrictions of functions. (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (𝐹 ↾ 𝑋) = (𝐺 ↾ 𝑋) ∧ (𝑌 ∈ dom 𝐹 ∧ 𝑌 ∈ dom 𝐺 ∧ (𝐹‘𝑌) = (𝐺‘𝑌))) → (𝐹 ↾ (𝑋 ∪ {𝑌})) = (𝐺 ↾ (𝑋 ∪ {𝑌})))
Theorem	eqfunressuc 7368	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 7369*	Condition for subset of an intersection of an image. (Contributed by Scott Fenton, 16-Aug-2024.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ⊆ ∩ (𝐹 “ 𝐵) ↔ ∀𝑥 ∈ 𝐵 𝐶 ⊆ (𝐹‘𝑥)))
Theorem	fnimasnd 7370	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 7371	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 9132. Note that 𝐴 must be a set: this theorem does not hold when 𝐴 is too large to be a set; see ncanth 7372 for a counterexample. (Use nex 1833 if you want the form ¬ ∃𝑓𝑓:𝐴–onto→𝒫 𝐴.) (Contributed by NM, 7-Aug-1994.) (Proof shortened by Mario Carneiro, 7-Jun-2016.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ¬ 𝐹:𝐴–onto→𝒫 𝐴
Theorem	ncanth 7372	Cantor's theorem fails for the universal class (which is not a set but a proper class by vprc 5281). Specifically, the identity function maps the universe onto its power class. Compare canth 7371 that works for sets. This failure comes from a limitation of the collection principle (which is necessary to avoid Russell's paradox ru 3741): 𝒫 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 4867). See also the remark in ru 3741 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 7373	Extend class notation with restricted description binder.
class (℩𝑥 ∈ 𝐴 𝜑)
Definition	df-riota 7374	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 6493. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 2-Sep-2018.)
⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	riotaeqdv 7375*	Formula-building deduction for iota. (Contributed by NM, 15-Sep-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐵 𝜓))
Theorem	riotabidv 7376*	Formula-building deduction for restricted iota. (Contributed by NM, 15-Sep-2011.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒))
Theorem	riotaeqbidv 7377*	Equality deduction for restricted universal quantifier. (Contributed by NM, 15-Sep-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐵 𝜒))
Theorem	riotaex 7378	Restricted iota is a set. (Contributed by NM, 15-Sep-2011.)
⊢ (℩𝑥 ∈ 𝐴 𝜓) ∈ V
Theorem	riotav 7379	An iota restricted to the universe is unrestricted. (Contributed by NM, 18-Sep-2011.)
⊢ (℩𝑥 ∈ V 𝜑) = (℩𝑥𝜑)
Theorem	riotauni 7380	Restricted iota in terms of class union. (Contributed by NM, 11-Oct-2011.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) = ∪ {𝑥 ∈ 𝐴 ∣ 𝜑})
Theorem	nfriota1 7381*	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 7382*	Deduction version of nfriota 7386 with a disjoint variable condition, which contrary to nfriotad 7385 does not require ax-13 2403. (Contributed by NM, 18-Feb-2013.) Avoid ax-13 2403. (Revised by GG, 26-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜓))
Theorem	cbvriotaw 7383*	Change bound variable in a restricted description binder. Version of cbvriota 7387 with a disjoint variable condition, which does not require ax-13 2403. (Contributed by NM, 18-Mar-2013.) Avoid ax-13 2403. (Revised by GG, 26-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓)
Theorem	cbvriotavw 7384*	Change bound variable in a restricted description binder. Version of cbvriotav 7388 with a disjoint variable condition, which requires fewer axioms . (Contributed by NM, 18-Mar-2013.) (Revised by GG, 30-Sep-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓)
Theorem	nfriotad 7385	Deduction version of nfriota 7386. Usage of this theorem is discouraged because it depends on ax-13 2403. Use the weaker nfriotadw 7382 when possible. (Contributed by NM, 18-Feb-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜓))
Theorem	nfriota 7386*	A variable not free in a wff remains so in a restricted iota descriptor. (Contributed by NM, 12-Oct-2011.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜑)
Theorem	cbvriota 7387*	Change bound variable in a restricted description binder. Usage of this theorem is discouraged because it depends on ax-13 2403. Use the weaker cbvriotaw 7383 when possible. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓)
Theorem	cbvriotav 7388*	Change bound variable in a restricted description binder. Usage of this theorem is discouraged because it depends on ax-13 2403. Use the weaker cbvriotavw 7384 when possible. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓)
Theorem	csbriota 7389*	Interchange class substitution and restricted description binder. (Contributed by NM, 24-Feb-2013.) (Revised by NM, 2-Sep-2018.)
⊢ ⦋𝐴 / 𝑥⦌(℩𝑦 ∈ 𝐵 𝜑) = (℩𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)
Theorem	riotacl2 7390	Membership law for "the unique element in 𝐴 such that 𝜑". (Contributed by NM, 21-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})
Theorem	riotacl 7391*	Closure of restricted iota. (Contributed by NM, 21-Aug-2011.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴)
Theorem	riotasbc 7392	Substitution law for descriptions. Compare iotasbc 45251. (Contributed by NM, 23-Aug-2011.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → [(℩𝑥 ∈ 𝐴 𝜑) / 𝑥]𝜑)
Theorem	riotabidva 7393*	Equivalent wff's yield equal restricted class abstractions (deduction form). (rabbidva 3420 analog.) (Contributed by NM, 17-Jan-2012.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒))
Theorem	riotabiia 7394	Equivalent wff's yield equal restricted iotas (inference form). (rabbiia 3418 analog.) (Contributed by NM, 16-Jan-2012.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐴 𝜓)
Theorem	riota1 7395*	Property of restricted iota. Compare iota1 6516. (Contributed by Mario Carneiro, 15-Oct-2016.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝑥))
Theorem	riota1a 7396	Property of iota. (Contributed by NM, 23-Aug-2011.)
⊢ ((𝑥 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜑 ↔ (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) = 𝑥))
Theorem	riota2df 7397*	A deduction version of riota2f 7398. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ ∃!𝑥 ∈ 𝐴 𝜓) → (𝜒 ↔ (℩𝑥 ∈ 𝐴 𝜓) = 𝐵))
Theorem	riota2f 7398*	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 7399*	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 7400*	If two restricted iota descriptors for an equality are equal, then the terms of the equality are equal. (Contributed by AV, 6-Dec-2020.)
⊢ 𝐼 = (℩𝑎 ∈ 𝑉 𝑋 = 𝐴)    &   ⊢ 𝐽 = (℩𝑎 ∈ 𝑉 𝑌 = 𝐴)    &   ⊢ (𝜑 → ∃!𝑎 ∈ 𝑉 𝑋 = 𝐴)    &   ⊢ (𝜑 → ∃!𝑎 ∈ 𝑉 𝑌 = 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝐼 = 𝐽) → 𝑋 = 𝑌)