P. 479 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 47801-47900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	adh-minimp-idALT 47801	Derivation of id 23 (reflexivity of implication, PM *2.08 WhiteheadRussell p. 101) from adh-minimp-ax1 47796, adh-minimp-ax2 47800, and ax-mp 5. It uses the derivation written DD211 in D-notation. (See head comment for an explanation.) Polish prefix notation: Cpp . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜑)
Theorem	adh-minimp-pm2.43 47802	Derivation of pm2.43 57 WhiteheadRussell p. 106 (also called "hilbert" or "W") from adh-minimp-ax1 47796, adh-minimp-ax2 47800, and ax-mp 5. It uses the derivation written DD22D21 in D-notation. (See head comment for an explanation.) Polish prefix notation: CCpCpqCpq . (Contributed by BJ, 31-May-2021.) (Revised by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜓))
21.49  Mathbox for Alexander van der Vekens
21.49.1  General auxiliary theorems (1)
21.49.1.1  Unordered and ordered pairs - extension for singletons
Theorem	n0nsn2el 47803*	If a class with one element is not a singleton, there is at least another element in this class. (Contributed by AV, 6-Mar-2025.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ≠ {𝐴}) → ∃𝑥 ∈ 𝐵 𝑥 ≠ 𝐴)
Theorem	eusnsn 47804*	There is a unique element of a singleton which is equal to another singleton. (Contributed by AV, 24-Aug-2022.)
⊢ ∃!𝑥{𝑥} = {𝑦}
Theorem	absnsb 47805*	If the class abstraction {𝑥 ∣ 𝜑} associated with the wff 𝜑 is a singleton, the wff is true for the singleton element. (Contributed by AV, 24-Aug-2022.)
⊢ ({𝑥 ∣ 𝜑} = {𝑦} → [𝑦 / 𝑥]𝜑)
Theorem	euabsneu 47806*	Another way to express existential uniqueness of a wff 𝜑: its associated class abstraction {𝑥 ∣ 𝜑} is a singleton. Variant of euabsn2 4696 using existential uniqueness for the singleton element instead of existence only. (Contributed by AV, 24-Aug-2022.)
⊢ (∃!𝑥𝜑 ↔ ∃!𝑦{𝑥 ∣ 𝜑} = {𝑦})
21.49.1.2  Unordered and ordered pairs - extension for unordered pairs
Theorem	elprneb 47807	An element of a proper unordered pair is the first element iff it is not the second element. (Contributed by AV, 18-Jun-2020.)
⊢ ((𝐴 ∈ {𝐵, 𝐶} ∧ 𝐵 ≠ 𝐶) → (𝐴 = 𝐵 ↔ 𝐴 ≠ 𝐶))
21.49.1.3  Unordered and ordered pairs - extension for ordered pairs
Theorem	oppr 47808	Equality for ordered pairs implies equality of unordered pairs with the same elements. (Contributed by AV, 9-Jul-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐴, 𝐵} = {𝐶, 𝐷}))
Theorem	opprb 47809	Equality for unordered pairs corresponds to equality of unordered pairs with the same elements. (Contributed by AV, 9-Jul-2023.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ∨ ⟨𝐴, 𝐵⟩ = ⟨𝐷, 𝐶⟩)))
Theorem	or2expropbilem1 47810*	Lemma 1 for or2expropbi 47812 and ich2exprop 48261. (Contributed by AV, 16-Jul-2023.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 = 𝑎 ∧ 𝐵 = 𝑏) → (𝜑 → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎]𝜑))))
Theorem	or2expropbilem2 47811*	Lemma 2 for or2expropbi 47812 and ich2exprop 48261. (Contributed by AV, 16-Jul-2023.)
⊢ (∃𝑎∃𝑏(⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎]𝜑))
Theorem	or2expropbi 47812*	If two classes are strictly ordered, there is an ordered pair of both classes fulfilling a wff iff there is an unordered pair of both classes fulfilling the wff. (Contributed by AV, 26-Aug-2023.)
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → (∃𝑎∃𝑏({𝐴, 𝐵} = {𝑎, 𝑏} ∧ (𝑎𝑅𝑏 ∧ 𝜑)) ↔ ∃𝑎∃𝑏(⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝑅𝑏 ∧ 𝜑))))
21.49.1.4  Relations - extension
Theorem	eubrv 47813*	If there is a unique set which is related to a class, then the class must be a set. (Contributed by AV, 25-Aug-2022.)
⊢ (∃!𝑏 𝐴𝑅𝑏 → 𝐴 ∈ V)
Theorem	eubrdm 47814*	If there is a unique set which is related to a class, then the class is an element of the domain of the relation. (Contributed by AV, 25-Aug-2022.)
⊢ (∃!𝑏 𝐴𝑅𝑏 → 𝐴 ∈ dom 𝑅)
Theorem	eldmressn 47815	Element of the domain of a restriction to a singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
⊢ (𝐵 ∈ dom (𝐹 ↾ {𝐴}) → 𝐵 = 𝐴)
21.49.1.5  Definite description binder (inverted iota) - extension
Theorem	iota0def 47816*	Example for a defined iota being the empty set, i.e., ∀𝑦𝑥 ⊆ 𝑦 is a wff satisfied by a unique value 𝑥, namely 𝑥 = ∅ (the empty set is the one and only set which is a subset of every set). (Contributed by AV, 24-Aug-2022.)
⊢ (℩𝑥∀𝑦 𝑥 ⊆ 𝑦) = ∅
Theorem	iota0ndef 47817*	Example for an undefined iota being the empty set, i.e., ∀𝑦𝑦 ∈ 𝑥 is a wff not satisfied by a (unique) value 𝑥 (there is no set, and therefore certainly no unique set, which contains every set). (Contributed by AV, 24-Aug-2022.)
⊢ (℩𝑥∀𝑦 𝑦 ∈ 𝑥) = ∅
21.49.1.6  Functions - extension
Theorem	fveqvfvv 47818	If a function's value at an argument is the universal class (which can never be the case because of fvex 6901), the function's value at this argument is any set (especially the empty set). In short "If a function's value is a proper class, it is a set", which sounds strange/contradictory, but which is a consequence of that a contradiction implies anything (see pm2.21i 120). (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ ((𝐹‘𝐴) = V → (𝐹‘𝐴) = 𝐵)
Theorem	fnresfnco 47819	Composition of two functions, similar to fnco 6660. (Contributed by Alexander van der Vekens, 25-Jul-2017.)
⊢ (((𝐹 ↾ ran 𝐺) Fn ran 𝐺 ∧ 𝐺 Fn 𝐵) → (𝐹 ∘ 𝐺) Fn 𝐵)
Theorem	funcoressn 47820	A composition restricted to a singleton is a function under certain conditions. (Contributed by Alexander van der Vekens, 25-Jul-2017.)
⊢ ((((𝐺‘𝑋) ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {(𝐺‘𝑋)})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → Fun ((𝐹 ∘ 𝐺) ↾ {𝑋}))
Theorem	funressnfv 47821	A restriction to a singleton with a function value is a function under certain conditions. (Contributed by Alexander van der Vekens, 25-Jul-2017.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → Fun (𝐹 ↾ {(𝐺‘𝑋)}))
Theorem	funressndmfvrn 47822	The value of a function 𝐹 at a set 𝐴 is in the range of the function 𝐹 if 𝐴 is in the domain of the function 𝐹. It is sufficient that 𝐹 is a function at 𝐴. (Contributed by AV, 1-Sep-2022.)
⊢ ((Fun (𝐹 ↾ {𝐴}) ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ ran 𝐹)
Theorem	funressnvmo 47823*	A function restricted to a singleton has at most one value for the singleton element as argument. (Contributed by AV, 2-Sep-2022.)
⊢ (Fun (𝐹 ↾ {𝑥}) → ∃*𝑦 𝑥𝐹𝑦)
Theorem	funressnmo 47824*	A function restricted to a singleton has at most one value for the singleton element as argument. (Contributed by AV, 2-Sep-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ Fun (𝐹 ↾ {𝐴})) → ∃*𝑦 𝐴𝐹𝑦)
Theorem	funressneu 47825*	There is exactly one value of a class which is a function restricted to a singleton, analogous to funeu 6568. 𝐴 ∈ V is required because otherwise ∃!𝑦𝐴𝐹𝑦, see brprcneu 6878. (Contributed by AV, 7-Sep-2022.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ Fun (𝐹 ↾ {𝐴}) ∧ 𝐴𝐹𝐵) → ∃!𝑦 𝐴𝐹𝑦)
Theorem	fresfo 47826	Conditions for a restriction to be an onto function. Part of fresf1o 33013. (Contributed by AV, 29-Sep-2024.)
⊢ ((Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹) → (𝐹 ↾ (◡𝐹 “ 𝐶)):(◡𝐹 “ 𝐶)–onto→𝐶)
Theorem	fsetsniunop 47827*	The class of all functions from a (proper) singleton into 𝐵 is the union of all the singletons of (proper) ordered pairs over the elements of 𝐵 as second component. (Contributed by AV, 13-Sep-2024.)
⊢ (𝑆 ∈ 𝑉 → {𝑓 ∣ 𝑓:{𝑆}⟶𝐵} = ∪ 𝑏 ∈ 𝐵 {{⟨𝑆, 𝑏⟩}})
Theorem	fsetabsnop 47828*	The class of all functions from a (proper) singleton into 𝐵 is the class of all the singletons of (proper) ordered pairs over the elements of 𝐵 as second component. (Contributed by AV, 13-Sep-2024.)
⊢ (𝑆 ∈ 𝑉 → {𝑓 ∣ 𝑓:{𝑆}⟶𝐵} = {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = {⟨𝑆, 𝑏⟩}})
Theorem	fsetsnf 47829*	The mapping of an element of a class to a singleton function is a function. (Contributed by AV, 13-Sep-2024.)
⊢ 𝐴 = {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = {⟨𝑆, 𝑏⟩}}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ {⟨𝑆, 𝑥⟩})    ⇒   ⊢ (𝑆 ∈ 𝑉 → 𝐹:𝐵⟶𝐴)
Theorem	fsetsnf1 47830*	The mapping of an element of a class to a singleton function is an injection. (Contributed by AV, 13-Sep-2024.)
⊢ 𝐴 = {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = {⟨𝑆, 𝑏⟩}}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ {⟨𝑆, 𝑥⟩})    ⇒   ⊢ (𝑆 ∈ 𝑉 → 𝐹:𝐵–1-1→𝐴)
Theorem	fsetsnfo 47831*	The mapping of an element of a class to a singleton function is a surjection. (Contributed by AV, 13-Sep-2024.)
⊢ 𝐴 = {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = {⟨𝑆, 𝑏⟩}}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ {⟨𝑆, 𝑥⟩})    ⇒   ⊢ (𝑆 ∈ 𝑉 → 𝐹:𝐵–onto→𝐴)
Theorem	fsetsnf1o 47832*	The mapping of an element of a class to a singleton function is a bijection. (Contributed by AV, 13-Sep-2024.)
⊢ 𝐴 = {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = {⟨𝑆, 𝑏⟩}}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ {⟨𝑆, 𝑥⟩})    ⇒   ⊢ (𝑆 ∈ 𝑉 → 𝐹:𝐵–1-1-onto→𝐴)
Theorem	fsetsnprcnex 47833*	The class of all functions from a (proper) singleton into a proper class 𝐵 is not a set. (Contributed by AV, 13-Sep-2024.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐵 ∉ V) → {𝑓 ∣ 𝑓:{𝑆}⟶𝐵} ∉ V)
Theorem	cfsetssfset 47834	The class of constant functions is a subclass of the class of functions. (Contributed by AV, 13-Sep-2024.)
⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏)}    ⇒   ⊢ 𝐹 ⊆ {𝑓 ∣ 𝑓:𝐴⟶𝐵}
Theorem	cfsetsnfsetfv 47835*	The function value of the mapping of the class of singleton functions into the class of constant functions. (Contributed by AV, 13-Sep-2024.)
⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏)}    &   ⊢ 𝐺 = {𝑥 ∣ 𝑥:{𝑌}⟶𝐵}    &   ⊢ 𝐻 = (𝑔 ∈ 𝐺 ↦ (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐺) → (𝐻‘𝑋) = (𝑎 ∈ 𝐴 ↦ (𝑋‘𝑌)))
Theorem	cfsetsnfsetf 47836*	The mapping of the class of singleton functions into the class of constant functions is a function. (Contributed by AV, 14-Sep-2024.)
⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏)}    &   ⊢ 𝐺 = {𝑥 ∣ 𝑥:{𝑌}⟶𝐵}    &   ⊢ 𝐻 = (𝑔 ∈ 𝐺 ↦ (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → 𝐻:𝐺⟶𝐹)
Theorem	cfsetsnfsetf1 47837*	The mapping of the class of singleton functions into the class of constant functions is an injection. (Contributed by AV, 14-Sep-2024.)
⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏)}    &   ⊢ 𝐺 = {𝑥 ∣ 𝑥:{𝑌}⟶𝐵}    &   ⊢ 𝐻 = (𝑔 ∈ 𝐺 ↦ (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → 𝐻:𝐺–1-1→𝐹)
Theorem	cfsetsnfsetfo 47838*	The mapping of the class of singleton functions into the class of constant functions is a surjection. (Contributed by AV, 14-Sep-2024.)
⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏)}    &   ⊢ 𝐺 = {𝑥 ∣ 𝑥:{𝑌}⟶𝐵}    &   ⊢ 𝐻 = (𝑔 ∈ 𝐺 ↦ (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → 𝐻:𝐺–onto→𝐹)
Theorem	cfsetsnfsetf1o 47839*	The mapping of the class of singleton functions into the class of constant functions is a bijection. (Contributed by AV, 14-Sep-2024.)
⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏)}    &   ⊢ 𝐺 = {𝑥 ∣ 𝑥:{𝑌}⟶𝐵}    &   ⊢ 𝐻 = (𝑔 ∈ 𝐺 ↦ (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → 𝐻:𝐺–1-1-onto→𝐹)
Theorem	fsetprcnexALT 47840*	First version of proof for fsetprcnex 8868, which was much more complicated. (Contributed by AV, 14-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∉ V) → {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∉ V)
Theorem	fcoreslem1 47841	Lemma 1 for fcores 47845. (Contributed by AV, 17-Sep-2024.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶)    &   ⊢ 𝑃 = (◡𝐹 “ 𝐶)    ⇒   ⊢ (𝜑 → 𝑃 = (◡𝐹 “ 𝐸))
Theorem	fcoreslem2 47842	Lemma 2 for fcores 47845. (Contributed by AV, 17-Sep-2024.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶)    &   ⊢ 𝑃 = (◡𝐹 “ 𝐶)    &   ⊢ 𝑋 = (𝐹 ↾ 𝑃)    ⇒   ⊢ (𝜑 → ran 𝑋 = 𝐸)
Theorem	fcoreslem3 47843	Lemma 3 for fcores 47845. (Contributed by AV, 13-Sep-2024.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶)    &   ⊢ 𝑃 = (◡𝐹 “ 𝐶)    &   ⊢ 𝑋 = (𝐹 ↾ 𝑃)    ⇒   ⊢ (𝜑 → 𝑋:𝑃–onto→𝐸)
Theorem	fcoreslem4 47844	Lemma 4 for fcores 47845. (Contributed by AV, 17-Sep-2024.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶)    &   ⊢ 𝑃 = (◡𝐹 “ 𝐶)    &   ⊢ 𝑋 = (𝐹 ↾ 𝑃)    &   ⊢ (𝜑 → 𝐺:𝐶⟶𝐷)    &   ⊢ 𝑌 = (𝐺 ↾ 𝐸)    ⇒   ⊢ (𝜑 → (𝑌 ∘ 𝑋) Fn 𝑃)
Theorem	fcores 47845	Every composite function (𝐺 ∘ 𝐹) can be written as composition of restrictions of the composed functions (to their minimum domains). (Contributed by GL and AV, 17-Sep-2024.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶)    &   ⊢ 𝑃 = (◡𝐹 “ 𝐶)    &   ⊢ 𝑋 = (𝐹 ↾ 𝑃)    &   ⊢ (𝜑 → 𝐺:𝐶⟶𝐷)    &   ⊢ 𝑌 = (𝐺 ↾ 𝐸)    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑌 ∘ 𝑋))
Theorem	fcoresf1lem 47846	Lemma for fcoresf1 47847. (Contributed by AV, 18-Sep-2024.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶)    &   ⊢ 𝑃 = (◡𝐹 “ 𝐶)    &   ⊢ 𝑋 = (𝐹 ↾ 𝑃)    &   ⊢ (𝜑 → 𝐺:𝐶⟶𝐷)    &   ⊢ 𝑌 = (𝐺 ↾ 𝐸)    ⇒   ⊢ ((𝜑 ∧ 𝑍 ∈ 𝑃) → ((𝐺 ∘ 𝐹)‘𝑍) = (𝑌‘(𝑋‘𝑍)))
Theorem	fcoresf1 47847	If a composition is injective, then the restrictions of its components to the minimum domains are injective. (Contributed by GL and AV, 18-Sep-2024.) (Revised by AV, 7-Oct-2024.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶)    &   ⊢ 𝑃 = (◡𝐹 “ 𝐶)    &   ⊢ 𝑋 = (𝐹 ↾ 𝑃)    &   ⊢ (𝜑 → 𝐺:𝐶⟶𝐷)    &   ⊢ 𝑌 = (𝐺 ↾ 𝐸)    &   ⊢ (𝜑 → (𝐺 ∘ 𝐹):𝑃–1-1→𝐷)    ⇒   ⊢ (𝜑 → (𝑋:𝑃–1-1→𝐸 ∧ 𝑌:𝐸–1-1→𝐷))
Theorem	fcoresf1b 47848	A composition is injective iff the restrictions of its components to the minimum domains are injective. (Contributed by GL and AV, 7-Oct-2024.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶)    &   ⊢ 𝑃 = (◡𝐹 “ 𝐶)    &   ⊢ 𝑋 = (𝐹 ↾ 𝑃)    &   ⊢ (𝜑 → 𝐺:𝐶⟶𝐷)    &   ⊢ 𝑌 = (𝐺 ↾ 𝐸)    ⇒   ⊢ (𝜑 → ((𝐺 ∘ 𝐹):𝑃–1-1→𝐷 ↔ (𝑋:𝑃–1-1→𝐸 ∧ 𝑌:𝐸–1-1→𝐷)))
Theorem	fcoresfo 47849	If a composition is surjective, then the restriction of its first component to the minimum domain is surjective. (Contributed by AV, 17-Sep-2024.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶)    &   ⊢ 𝑃 = (◡𝐹 “ 𝐶)    &   ⊢ 𝑋 = (𝐹 ↾ 𝑃)    &   ⊢ (𝜑 → 𝐺:𝐶⟶𝐷)    &   ⊢ 𝑌 = (𝐺 ↾ 𝐸)    &   ⊢ (𝜑 → (𝐺 ∘ 𝐹):𝑃–onto→𝐷)    ⇒   ⊢ (𝜑 → 𝑌:𝐸–onto→𝐷)
Theorem	fcoresfob 47850	A composition is surjective iff the restriction of its first component to the minimum domain is surjective. (Contributed by GL and AV, 7-Oct-2024.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶)    &   ⊢ 𝑃 = (◡𝐹 “ 𝐶)    &   ⊢ 𝑋 = (𝐹 ↾ 𝑃)    &   ⊢ (𝜑 → 𝐺:𝐶⟶𝐷)    &   ⊢ 𝑌 = (𝐺 ↾ 𝐸)    ⇒   ⊢ (𝜑 → ((𝐺 ∘ 𝐹):𝑃–onto→𝐷 ↔ 𝑌:𝐸–onto→𝐷))
Theorem	fcoresf1ob 47851	A composition is bijective iff the restriction of its first component to the minimum domain is bijective and the restriction of its second component to the minimum domain is injective. (Contributed by GL and AV, 7-Oct-2024.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶)    &   ⊢ 𝑃 = (◡𝐹 “ 𝐶)    &   ⊢ 𝑋 = (𝐹 ↾ 𝑃)    &   ⊢ (𝜑 → 𝐺:𝐶⟶𝐷)    &   ⊢ 𝑌 = (𝐺 ↾ 𝐸)    ⇒   ⊢ (𝜑 → ((𝐺 ∘ 𝐹):𝑃–1-1-onto→𝐷 ↔ (𝑋:𝑃–1-1→𝐸 ∧ 𝑌:𝐸–1-1-onto→𝐷)))
Theorem	f1cof1blem 47852	Lemma for f1cof1b 47855 and focofob 47858. (Contributed by AV, 18-Sep-2024.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶)    &   ⊢ 𝑃 = (◡𝐹 “ 𝐶)    &   ⊢ 𝑋 = (𝐹 ↾ 𝑃)    &   ⊢ (𝜑 → 𝐺:𝐶⟶𝐷)    &   ⊢ 𝑌 = (𝐺 ↾ 𝐸)    &   ⊢ (𝜑 → ran 𝐹 = 𝐶)    ⇒   ⊢ (𝜑 → ((𝑃 = 𝐴 ∧ 𝐸 = 𝐶) ∧ (𝑋 = 𝐹 ∧ 𝑌 = 𝐺)))
Theorem	3f1oss1 47853	The composition of three bijections as bijection from the image of the domain onto the image of the range of the middle bijection. (Contributed by AV, 15-Aug-2025.)
⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → ((𝐻 ∘ 𝐺) ∘ ◡𝐹):(𝐹 “ 𝐶)–1-1-onto→(𝐻 “ 𝐷))
Theorem	3f1oss2 47854	The composition of three bijections as bijection from the image of the converse of the domain onto the image of the converse of the range of the middle bijection. (Contributed by AV, 15-Aug-2025.)
⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐼)) → ((◡𝐻 ∘ 𝐺) ∘ 𝐹):(◡𝐹 “ 𝐶)–1-1-onto→(◡𝐻 “ 𝐷))
Theorem	f1cof1b 47855	If the range of 𝐹 equals the domain of 𝐺, then the composition (𝐺 ∘ 𝐹) is injective iff 𝐹 and 𝐺 are both injective. (Contributed by GL and AV, 19-Sep-2024.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐶⟶𝐷 ∧ ran 𝐹 = 𝐶) → ((𝐺 ∘ 𝐹):𝐴–1-1→𝐷 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐶–1-1→𝐷)))
Theorem	funfocofob 47856	If the domain of a function 𝐺 is a subset of the range of a function 𝐹, then the composition (𝐺 ∘ 𝐹) is surjective iff 𝐺 is surjective. (Contributed by GL and AV, 29-Sep-2024.)
⊢ ((Fun 𝐹 ∧ 𝐺:𝐴⟶𝐵 ∧ 𝐴 ⊆ ran 𝐹) → ((𝐺 ∘ 𝐹):(◡𝐹 “ 𝐴)–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
Theorem	fnfocofob 47857	If the domain of a function 𝐺 equals the range of a function 𝐹, then the composition (𝐺 ∘ 𝐹) is surjective iff 𝐺 is surjective. (Contributed by GL and AV, 29-Sep-2024.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺:𝐵⟶𝐶 ∧ ran 𝐹 = 𝐵) → ((𝐺 ∘ 𝐹):𝐴–onto→𝐶 ↔ 𝐺:𝐵–onto→𝐶))
Theorem	focofob 47858	If the domain of a function 𝐺 equals the range of a function 𝐹, then the composition (𝐺 ∘ 𝐹) is surjective iff 𝐺 and 𝐹 as function to the domain of 𝐺 are both surjective. Symmetric version of fnfocofob 47857 including the fact that 𝐹 is a surjection onto its range. (Contributed by GL and AV, 20-Sep-2024.) (Proof shortened by AV, 29-Sep-2024.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐶⟶𝐷 ∧ ran 𝐹 = 𝐶) → ((𝐺 ∘ 𝐹):𝐴–onto→𝐷 ↔ (𝐹:𝐴–onto→𝐶 ∧ 𝐺:𝐶–onto→𝐷)))
Theorem	f1ocof1ob 47859	If the range of 𝐹 equals the domain of 𝐺, then the composition (𝐺 ∘ 𝐹) is bijective iff 𝐹 and 𝐺 are both bijective. (Contributed by GL and AV, 7-Oct-2024.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐶⟶𝐷 ∧ ran 𝐹 = 𝐶) → ((𝐺 ∘ 𝐹):𝐴–1-1-onto→𝐷 ↔ (𝐹:𝐴–1-1→𝐶 ∧ 𝐺:𝐶–1-1-onto→𝐷)))
Theorem	f1ocof1ob2 47860	If the range of 𝐹 equals the domain of 𝐺, then the composition (𝐺 ∘ 𝐹) is bijective iff 𝐹 and 𝐺 are both bijective. Symmetric version of f1ocof1ob 47859 including the fact that 𝐹 is a surjection onto its range. (Contributed by GL and AV, 20-Sep-2024.) (Proof shortened by AV, 7-Oct-2024.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐶⟶𝐷 ∧ ran 𝐹 = 𝐶) → ((𝐺 ∘ 𝐹):𝐴–1-1-onto→𝐷 ↔ (𝐹:𝐴–1-1-onto→𝐶 ∧ 𝐺:𝐶–1-1-onto→𝐷)))
21.49.2  Alternative for Russell's definition of a description binder
Syntax	caiota 47861	Extend class notation with an alternative for Russell's definition of a description binder (inverted iota).
class (℩'𝑥𝜑)
Theorem	aiotajust 47862*	Soundness justification theorem for df-aiota 47863. (Contributed by AV, 24-Aug-2022.)
⊢ ∩ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = ∩ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}}
Definition	df-aiota 47863*	Alternate version of Russell's definition of a description binder, which can be read as "the unique 𝑥 such that 𝜑", where 𝜑 ordinarily contains 𝑥 as a free variable. Our definition is meaningful only when there is exactly one 𝑥 such that 𝜑 is true (see aiotaval 47873); otherwise, it is not a set (see aiotaexb 47867), or even more concrete, it is the universe V (see aiotavb 47868). Since this is an alternative for df-iota 6499, we call this symbol ℩' alternate iota in the following. The advantage of this definition is the clear distinguishability of the defined and undefined cases: the alternate iota over a wff is defined iff it is a set (see aiotaexb 47867). With the original definition, there is no corresponding theorem (∃!𝑥𝜑 ↔ (℩𝑥𝜑) ≠ ∅), because ∅ can be a valid unique set satisfying a wff (see, for example, iota0def 47816). Only the right to left implication would hold, see (negated) iotanul 6523. For defined cases, however, both definitions df-iota 6499 and df-aiota 47863 are equivalent, see reuaiotaiota 47866. (Proposed by BJ, 13-Aug-2022.) (Contributed by AV, 24-Aug-2022.)
⊢ (℩'𝑥𝜑) = ∩ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}}
Theorem	dfaiota2 47864*	Alternate definition of the alternate version of Russell's definition of a description binder. Definition 8.18 in [Quine] p. 56. (Contributed by AV, 24-Aug-2022.)
⊢ (℩'𝑥𝜑) = ∩ {𝑦 ∣ ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)}
Theorem	reuabaiotaiota 47865*	The iota and the alternate iota over a wff 𝜑 are equal iff there is a unique satisfying value of {𝑥 ∣ 𝜑} = {𝑦}. (Contributed by AV, 25-Aug-2022.)
⊢ (∃!𝑦{𝑥 ∣ 𝜑} = {𝑦} ↔ (℩𝑥𝜑) = (℩'𝑥𝜑))
Theorem	reuaiotaiota 47866	The iota and the alternate iota over a wff 𝜑 are equal iff there is a unique value 𝑥 satisfying 𝜑. (Contributed by AV, 25-Aug-2022.)
⊢ (∃!𝑥𝜑 ↔ (℩𝑥𝜑) = (℩'𝑥𝜑))
Theorem	aiotaexb 47867	The alternate iota over a wff 𝜑 is a set iff there is a unique value 𝑥 satisfying 𝜑. (Contributed by AV, 25-Aug-2022.)
⊢ (∃!𝑥𝜑 ↔ (℩'𝑥𝜑) ∈ V)
Theorem	aiotavb 47868	The alternate iota over a wff 𝜑 is the universe iff there is no unique value 𝑥 satisfying 𝜑. (Contributed by AV, 25-Aug-2022.)
⊢ (¬ ∃!𝑥𝜑 ↔ (℩'𝑥𝜑) = V)
Theorem	aiotaint 47869	This is to df-aiota 47863 what iotauni 6520 is to df-iota 6499 (it uses intersection like df-aiota 47863, similar to iotauni 6520 using union like df-iota 6499; we could also prove an analogous result using union here too, in the same way that we have iotaint 6521). (Contributed by BJ, 31-Aug-2024.)
⊢ (∃!𝑥𝜑 → (℩'𝑥𝜑) = ∩ {𝑥 ∣ 𝜑})
Theorem	dfaiota3 47870	Alternate definition of ℩', using the if operator: this is to df-aiota 47863 what dfiota4 6535 is to df-iota 6499. It is simpler than df-aiota 47863 and uses no dummy variables, so it would be the preferred definition if ℩' becomes the description binder used in set.mm. (Contributed by BJ, 31-Aug-2024.)
⊢ (℩'𝑥𝜑) = if(∃!𝑥𝜑, ∩ {𝑥 ∣ 𝜑}, V)
Theorem	iotan0aiotaex 47871	If the iota over a wff 𝜑 is not empty, the alternate iota over 𝜑 is a set. (Contributed by AV, 25-Aug-2022.)
⊢ ((℩𝑥𝜑) ≠ ∅ → (℩'𝑥𝜑) ∈ V)
Theorem	aiotaexaiotaiota 47872	The alternate iota over a wff 𝜑 is a set iff the iota and the alternate iota over 𝜑 are equal. (Contributed by AV, 25-Aug-2022.)
⊢ ((℩'𝑥𝜑) ∈ V ↔ (℩𝑥𝜑) = (℩'𝑥𝜑))
Theorem	aiotaval 47873*	Theorem 8.19 in [Quine] p. 57. This theorem is the fundamental property of (alternate) iota. (Contributed by AV, 24-Aug-2022.)
⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → (℩'𝑥𝜑) = 𝑦)
Theorem	aiota0def 47874*	Example for a defined alternate iota being the empty set, i.e., ∀𝑦𝑥 ⊆ 𝑦 is a wff satisfied by a unique value 𝑥, namely 𝑥 = ∅ (the empty set is the one and only set which is a subset of every set). This corresponds to iota0def 47816. (Contributed by AV, 25-Aug-2022.)
⊢ (℩'𝑥∀𝑦 𝑥 ⊆ 𝑦) = ∅
Theorem	aiota0ndef 47875*	Example for an undefined alternate iota being no set, i.e., ∀𝑦𝑦 ∈ 𝑥 is a wff not satisfied by a (unique) value 𝑥 (there is no set, and therefore certainly no unique set, which contains every set). This is different from iota0ndef 47817, where the iota still is a set (the empty set). (Contributed by AV, 25-Aug-2022.)
⊢ (℩'𝑥∀𝑦 𝑦 ∈ 𝑥) ∉ V
21.49.3  Double restricted existential uniqueness
21.49.3.1  Restricted quantification (extension)
Theorem	r19.32 47876	Theorem 19.32 of [Margaris] p. 90 with restricted quantifiers, analogous to r19.32v 3201. (Contributed by Alexander van der Vekens, 29-Jun-2017.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∀𝑥 ∈ 𝐴 𝜓))
Theorem	rexsb 47877*	An equivalent expression for restricted existence, analogous to exsb 2394. (Contributed by Alexander van der Vekens, 1-Jul-2017.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	rexrsb 47878*	An equivalent expression for restricted existence, analogous to exsb 2394. (Contributed by Alexander van der Vekens, 1-Jul-2017.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 = 𝑦 → 𝜑))
Theorem	2rexsb 47879*	An equivalent expression for double restricted existence, analogous to rexsb 47877. (Contributed by Alexander van der Vekens, 1-Jul-2017.)
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑))
Theorem	2rexrsb 47880*	An equivalent expression for double restricted existence, analogous to 2exsb 2395. (Contributed by Alexander van der Vekens, 1-Jul-2017.)
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑))
Theorem	cbvral2 47881*	Change bound variables of double restricted universal quantification, using implicit substitution, analogous to cbvral2v 3360. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ Ⅎ𝑤𝜒    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓)
Theorem	cbvrex2 47882*	Change bound variables of double restricted universal quantification, using implicit substitution, analogous to cbvrex2v 3361. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ Ⅎ𝑤𝜒    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓)
Theorem	ralndv1 47883	Example for a theorem about a restricted universal quantification in which the restricting class depends on (actually is) the bound variable: All sets containing themselves contain the universal class. (Contributed by AV, 24-Jun-2023.)
⊢ ∀𝑥 ∈ 𝑥 V ∈ 𝑥
Theorem	ralndv2 47884	Second example for a theorem about a restricted universal quantification in which the restricting class depends on the bound variable: all subsets of a set are sets. (Contributed by AV, 24-Jun-2023.)
⊢ ∀𝑥 ∈ 𝒫 𝑥𝑥 ∈ V
21.49.3.2  Restricted uniqueness and "at most one" quantification
Theorem	reuf1odnf 47885*	There is exactly one element in each of two isomorphic sets. Variant of reuf1od 47886 with no distinct variable condition for 𝜒. (Contributed by AV, 19-Mar-2023.)
⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑧 → (𝜓 ↔ 𝜃))    &   ⊢ Ⅎ𝑥𝜒    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 𝜓 ↔ ∃!𝑦 ∈ 𝐶 𝜒))
Theorem	reuf1od 47886*	There is exactly one element in each of two isomorphic sets. (Contributed by AV, 19-Mar-2023.)
⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 𝜓 ↔ ∃!𝑦 ∈ 𝐶 𝜒))
Theorem	euoreqb 47887*	There is a set which is equal to one of two other sets iff the other sets are equal. (Contributed by AV, 24-Jan-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (∃!𝑥 ∈ 𝑉 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ 𝐴 = 𝐵))
21.49.3.3  Analogs to Existential uniqueness (double quantification)
Theorem	2reu3 47888*	Double restricted existential uniqueness, analogous to 2eu3 2684. (Contributed by Alexander van der Vekens, 29-Jun-2017.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (∃*𝑥 ∈ 𝐴 𝜑 ∨ ∃*𝑦 ∈ 𝐵 𝜑) → ((∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝜑) ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)))
Theorem	2reu7 47889*	Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu7 2688. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
⊢ ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ ∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜑))
Theorem	2reu8 47890*	Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu8 2689. Curiously, we can put ∃! on either of the internal conjuncts but not both. We can also commute ∃!𝑥 ∈ 𝐴∃!𝑦 ∈ 𝐵 using 2reu7 47889. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
⊢ (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜑) ↔ ∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 (∃!𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜑))
21.49.3.4  Additional theorems for double restricted existential uniqueness
Theorem	2reu8i 47891*	Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification, see also 2reu8 47890. The involved wffs depend on the setvar variables as follows: ph(x,y), ta(v,y), ch(x,w), th(v,w), et(x,b), ps(a,b), ze(a,w). (Contributed by AV, 1-Apr-2023.)
⊢ (𝑥 = 𝑣 → (𝜑 ↔ 𝜏))    &   ⊢ (𝑥 = 𝑣 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑦 = 𝑤 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑏 → (𝜑 ↔ 𝜂))    &   ⊢ (𝑥 = 𝑎 → (𝜒 ↔ 𝜁))    &   ⊢ (((𝜒 → 𝑦 = 𝑤) ∧ 𝜁) → 𝑦 = 𝑤)    &   ⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))
Theorem	2reuimp0 47892*	Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification. The involved wffs depend on the setvar variables as follows: ph(a,b), th(a,c), ch(d,b), ta(d,c), et(a,e), ps(a,f) (Contributed by AV, 13-Mar-2023.)
⊢ (𝑏 = 𝑐 → (𝜑 ↔ 𝜃))    &   ⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑎 = 𝑑 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑏 = 𝑒 → (𝜑 ↔ 𝜂))    &   ⊢ (𝑐 = 𝑓 → (𝜃 ↔ 𝜓))    ⇒   ⊢ (∃!𝑎 ∈ 𝑉 ∃!𝑏 ∈ 𝑉 𝜑 → ∃𝑎 ∈ 𝑉 ∀𝑑 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))
Theorem	2reuimp 47893*	Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification if the class of the quantified elements is not empty. (Contributed by AV, 13-Mar-2023.)
⊢ (𝑏 = 𝑐 → (𝜑 ↔ 𝜃))    &   ⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑎 = 𝑑 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑏 = 𝑒 → (𝜑 ↔ 𝜂))    &   ⊢ (𝑐 = 𝑓 → (𝜃 ↔ 𝜓))    ⇒   ⊢ ((𝑉 ≠ ∅ ∧ ∃!𝑎 ∈ 𝑉 ∃!𝑏 ∈ 𝑉 𝜑) → ∃𝑎 ∈ 𝑉 ∀𝑑 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ((𝜒 ∧ (𝜏 → 𝑏 = 𝑐)) → (𝜓 → (𝜂 ∧ (𝑎 = 𝑑 ∧ 𝑒 = 𝑓)))))
21.49.4  Alternative definitions of function and operation values The current definition of the value (𝐹‘𝐴) of a function 𝐹 at an argument 𝐴 (see df-fv 6551) assures that this value is always a set, see fex 7231. This is because this definition can be applied to any classes 𝐹 and 𝐴, and evaluates to the empty set when it is not meaningful (as shown by ndmfv 6920 and fvprc 6880). Although it is very convenient for many theorems on functions and their proofs, there are some cases in which from (𝐹‘𝐴) = ∅ alone it cannot be decided/derived whether (𝐹‘𝐴) is meaningful (𝐹 is actually a function which is defined for 𝐴 and really has the function value ∅ at 𝐴) or not. Therefore, additional assumptions are required, such as ∅ ∉ ran 𝐹, ∅ ∈ ran 𝐹 or Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 (see, for example, ndmfvrcl 6921). To avoid such an ambiguity, an alternative definition (𝐹'''𝐴) (see df-afv 47898) would be possible which evaluates to the universal class ((𝐹'''𝐴) = V) if it is not meaningful (see afvnfundmuv 47917, ndmafv 47918, afvprc 47922 and nfunsnafv 47920), and which corresponds to the current definition ((𝐹‘𝐴) = (𝐹'''𝐴)) if it is (see afvfundmfveq 47916). That means (𝐹'''𝐴) = V → (𝐹‘𝐴) = ∅ (see afvpcfv0 47924), but (𝐹‘𝐴) = ∅ → (𝐹'''𝐴) = V is not generally valid. In the theory of partial functions, it is a common case that 𝐹 is not defined at 𝐴, which also would result in (𝐹'''𝐴) = V. In this context we say (𝐹'''𝐴) "is not defined" instead of "is not meaningful". With this definition the following intuitive equivalence holds: (𝐹'''𝐴) ∈ V <-> "(𝐹'''𝐴) is meaningful/defined". An interesting question would be if (𝐹‘𝐴) could be replaced by (𝐹'''𝐴) in most of the theorems based on function values. If we look at the (currently 19) proofs using the definition df-fv 6551 of (𝐹‘𝐴), we see that analogues for the following 8 theorems can be proven using the alternative definition: fveq1 6887-> afveq1 47912, fveq2 6888-> afveq2 47913, nffv 6898-> nfafv 47914, csbfv12 6933-> csbafv12g , fvres 6907-> afvres 47950, rlimdm 15628-> rlimdmafv 47955, tz6.12-1 6911-> tz6.12-1-afv 47952, fveu 6877-> afveu 47931. Three theorems proved by directly using df-fv 6551 are within a mathbox (fvsb 45201) or not used (isumclim3 15836, avril1 30851). However, the remaining 8 theorems proved by directly using df-fv 6551 are used more or less often: * fvex 6901: used in about 1750 proofs. * tz6.12-1 6911: root theorem of many theorems which have not a strict analogue, and which are used many times: fvprc 6880 (used in about 127 proofs), tz6.12i 6914 (used - indirectly via fvbr0 6915 and fvrn0 6916- in 18 proofs, and in fvclss 7246 used in fvclex 7965 used in fvresex 7966, which is not used!), dcomex 10449 (used in 4 proofs), ndmfv 6920 (used in 86 proofs) and nfunsn 6927 (used by dffv2 6983 which is not used). * fv2 6883: only used by elfv 6886, which is only used by fv3 6906, which is not used. * dffv3 6884: used by dffv4 6885 (the previous "df-fv"), which now is only used in deprecated (usage discouraged) theorems or within mathboxes (csbfv12gALTVD 45648), by shftval 15137 (itself used in 9 proofs), by dffv5 36435 (mathbox) and by fvco2 6985, which has the analogue afvco2 47954. * fvopab5 7030: used only by ajval 31250 (not used) and by adjval 32279 (used - indirectly - in 9 proofs). * zsum 15795: used (via isum 15796, sum0 15798 and fsumsers 15805) in more than 90 proofs. * isumshft 15919: used in pserdv2 26630 and (via logtayl 26862) 4 other proofs. * ovtpos 8246: used in 14 proofs. As a result of this analysis we can say that the current definition of a function value is crucial for Metamath and cannot be exchanged easily with an alternative definition. While fv2 6883, dffv3 6884, fvopab5 7030, zsum 15795, isumshft 15919 and ovtpos 8246 are not critical or are, hopefully, also valid for the alternative definition, fvex 6901 and tz6.12-1 6911 (and the theorems based on them) are essential for the current definition of function values. With the same arguments, an alternative definition of operation values ((𝐴𝑂𝐵)) could be meaningful to avoid ambiguities, see df-aov 47899. For additional details, see https://groups.google.com/g/metamath/c/cteNUppB6A4 47899.
Syntax	wdfat 47894	Extend the definition of a wff to include the "defined at" predicate. Read: "(the function) 𝐹 is defined at (the argument) 𝐴". In a previous version, the token "def@" was used. However, since the @ is used (informally) as a replacement for $ in commented out sections that may be deleted some day. While there is no violation of any standard to use the @ in a token, it could make the search for such commented-out sections slightly more difficult. (See remark of Norman Megill at https://groups.google.com/g/metamath/c/cteNUppB6A4).
wff 𝐹 defAt 𝐴
Syntax	cafv 47895	Extend the definition of a class to include the value of a function. Read: "the value of 𝐹 at 𝐴 " or "𝐹 of 𝐴". In a previous version, the symbol " ' " was used. However, since the similarity with the symbol ‘ used for the current definition of a function's value (see df-fv 6551), which, by the way, was intended to visualize that in many cases ‘ and " ' " are exchangeable, makes reading the theorems, especially those which use both definitions as dfafv2 47910, very difficult, 3 apostrophes ''' are used now so that it's easier to distinguish from df-fv 6551 and df-ima 5679. And not three backticks ( three times ‘) since that would be annoying to escape in a comment. (See remark of Norman Megill and Gerard Lang at https://groups.google.com/g/metamath/c/cteNUppB6A4 5679).
class (𝐹'''𝐴)
Syntax	caov 47896	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 a pair of parentheses in contrast to the current definition, see df-ov 7426.
class ((𝐴𝐹𝐵))
Definition	df-dfat 47897	Definition of the predicate that determines if some class 𝐹 is defined as function for an argument 𝐴 or, in other words, if the function value for some class 𝐹 for an argument 𝐴 is defined. We say that 𝐹 is defined at 𝐴 if a 𝐹 is a function restricted to the member 𝐴 of its domain. (Contributed by Alexander van der Vekens, 25-May-2017.)
⊢ (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))
Definition	df-afv 47898*	Alternative definition of the value of a function, (𝐹'''𝐴), also known as function application. In contrast to (𝐹‘𝐴) = ∅ (see df-fv 6551 and ndmfv 6920), (𝐹'''𝐴) = V if F is not defined for A! (Contributed by Alexander van der Vekens, 25-May-2017.) (Revised by BJ/AV, 25-Aug-2022.)
⊢ (𝐹'''𝐴) = (℩'𝑥𝐴𝐹𝑥)
Definition	df-aov 47899	Define the value of an operation. In contrast to df-ov 7426, the alternative definition for a function value (see df-afv 47898) is used. By this, the value of the operation applied to two arguments is the universal class if the operation is not defined for these two arguments. There are still 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. (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ ((𝐴𝐹𝐵)) = (𝐹'''⟨𝐴, 𝐵⟩)
21.49.4.1  Restricted quantification (extension)
Theorem	ralbinrald 47900*	Elemination of a restricted universal quantification under certain conditions. (Contributed by Alexander van der Vekens, 2-Aug-2017.)
⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝑥 ∈ 𝐴 → 𝑥 = 𝑋)    &   ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ 𝜃))