P. 494 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49301-49400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mpbiran3d 49301	Equivalence with a conjunction one of whose conjuncts is a consequence of the other. Deduction form. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜒))
Theorem	mpbiran4d 49302	Equivalence with a conjunction one of whose conjuncts is a consequence of the other. Deduction form. (Contributed by Zhi Wang, 27-Sep-2024.)
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜒)    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜃))
21.49.2  Predicate calculus with equality
21.49.2.1  Axiom scheme ax-5 (Distinctness)
Theorem	dtrucor3 49303*	An example of how ax-5 1918 without a distinct variable condition causes paradox in models of at least two objects. The hypothesis "dtrucor3.1" is provable from dtru 5379 in the ZF set theory. axc16nf 2277 and euae 2665 demonstrate that the violation of dtru 5379 leads to a model with only one object assuming its existence (ax-6 1975). The conclusion is also provable in the empty model ( see emptyal 1916). See also nf5 2295 and nf5i 2159 for the relation between unconditional ax-5 1918 and being not free. (Contributed by Zhi Wang, 23-Sep-2024.)
⊢ ¬ ∀𝑥 𝑥 = 𝑦    &   ⊢ (𝑥 = 𝑦 → ∀𝑥 𝑥 = 𝑦)    ⇒   ⊢ ∀𝑥 𝑥 = 𝑦
21.49.3  ZF Set Theory - start with the Axiom of Extensionality
21.49.3.1  Restricted quantification
Theorem	ralbidb 49304*	Formula-building rule for restricted universal quantifier and additional condition (deduction form). See ralbidc 49305 for a more generalized form. (Contributed by Zhi Wang, 6-Sep-2024.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜓)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜒 ↔ 𝜃))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜒 ↔ ∀𝑥 ∈ 𝐵 (𝜓 → 𝜃)))
Theorem	ralbidc 49305*	Formula-building rule for restricted universal quantifier and additional condition (deduction form). A variant of ralbidb 49304. (Contributed by Zhi Wang, 30-Aug-2024.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜓)))    &   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) → (𝜒 ↔ 𝜃)))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜒 ↔ ∀𝑥 ∈ 𝐵 (𝜓 → 𝜃)))
Theorem	r19.41dv 49306*	A complex deduction form of r19.41v 3171. (Contributed by Zhi Wang, 6-Sep-2024.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒))
Theorem	rmotru 49307	Two ways of expressing "at most one" element. (Contributed by Zhi Wang, 19-Sep-2024.) (Proof shortened by BJ, 23-Sep-2024.)
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∃*𝑥 ∈ 𝐴 ⊤)
Theorem	reutru 49308	Two ways of expressing "exactly one" element. (Contributed by Zhi Wang, 23-Sep-2024.)
⊢ (∃!𝑥 𝑥 ∈ 𝐴 ↔ ∃!𝑥 ∈ 𝐴 ⊤)
Theorem	reutruALT 49309	Alternate proof of reutru 49308. (Contributed by Zhi Wang, 23-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃!𝑥 𝑥 ∈ 𝐴 ↔ ∃!𝑥 ∈ 𝐴 ⊤)
Theorem	reueqbidva 49310*	Formula-building rule for restricted existential uniqueness quantifier. Deduction form. General version of reueqbidv 3382. (Contributed by Zhi Wang, 20-Nov-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐵 𝜒))
21.49.3.2  The universal class
Theorem	reuxfr1dd 49311*	Transfer existential uniqueness from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. Simplifies reuxfr1d 3693. (Contributed by Zhi Wang, 20-Sep-2025.)
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃!𝑦 ∈ 𝐶 𝑥 = 𝐴)    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐴)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 𝜓 ↔ ∃!𝑦 ∈ 𝐶 𝜒))
21.49.3.3  The empty set
Theorem	ssdisjd 49312	Subset preserves disjointness. Deduction form of ssdisj 4391. (Contributed by Zhi Wang, 7-Sep-2024.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → (𝐵 ∩ 𝐶) = ∅)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐶) = ∅)
Theorem	ssdisjdr 49313	Subset preserves disjointness. Deduction form of ssdisj 4391. Alternatively this could be proved with ineqcom 4142 in tandem with ssdisjd 49312. (Contributed by Zhi Wang, 7-Sep-2024.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → (𝐶 ∩ 𝐵) = ∅)    ⇒   ⊢ (𝜑 → (𝐶 ∩ 𝐴) = ∅)
Theorem	disjdifb 49314	Relative complement is anticommutative regarding intersection. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ ((𝐴 ∖ 𝐵) ∩ (𝐵 ∖ 𝐴)) = ∅
Theorem	predisj 49315	Preimages of disjoint sets are disjoint. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → 𝑆 ⊆ (◡𝐹 “ 𝐴))    &   ⊢ (𝜑 → 𝑇 ⊆ (◡𝐹 “ 𝐵))    ⇒   ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅)
21.49.3.4  Unordered and ordered pairs
Theorem	vsn 49316	The singleton of the universal class is the empty set. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ {V} = ∅
Theorem	mosn 49317*	"At most one" element in a singleton. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ (𝐴 = {𝐵} → ∃*𝑥 𝑥 ∈ 𝐴)
Theorem	mo0 49318*	"At most one" element in an empty set. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ (𝐴 = ∅ → ∃*𝑥 𝑥 ∈ 𝐴)
Theorem	mosssn 49319*	"At most one" element in a subclass of a singleton. (Contributed by Zhi Wang, 23-Sep-2024.)
⊢ (𝐴 ⊆ {𝐵} → ∃*𝑥 𝑥 ∈ 𝐴)
Theorem	mo0sn 49320*	Two ways of expressing "at most one" element in a class. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ (𝐴 = ∅ ∨ ∃𝑦 𝐴 = {𝑦}))
Theorem	mosssn2 49321*	Two ways of expressing "at most one" element in a class. (Contributed by Zhi Wang, 23-Sep-2024.)
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∃𝑦 𝐴 ⊆ {𝑦})
21.49.3.5  The union of a class
Theorem	unilbss 49322*	Superclass of the greatest lower bound. A dual statement of ssintub 4899. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴} ⊆ 𝐴
21.49.3.6  Indexed union and intersection
Theorem	iuneq0 49323	An indexed union is empty iff all indexed classes are empty. (Contributed by Zhi Wang, 1-Nov-2025.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 = ∅ ↔ ∪ 𝑥 ∈ 𝐴 𝐵 = ∅)
Theorem	iineq0 49324	An indexed intersection is empty if one of the intersected classes is empty. (Contributed by Zhi Wang, 30-Oct-2025.)
⊢ (∃𝑥 ∈ 𝐴 𝐵 = ∅ → ∩ 𝑥 ∈ 𝐴 𝐵 = ∅)
Theorem	iunlub 49325*	The indexed union is the the lowest upper bound if it exists. (Contributed by Zhi Wang, 1-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = 𝐶)
Theorem	iinglb 49326*	The indexed intersection is the the greatest lower bound if it exists. (Contributed by Zhi Wang, 1-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 = 𝐶)
Theorem	iuneqconst2 49327*	Indexed union of identical classes. (Contributed by Zhi Wang, 6-Nov-2025.)
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → ∪ 𝑥 ∈ 𝐴 𝐵 = 𝐶)
Theorem	iineqconst2 49328*	Indexed intersection of identical classes. (Contributed by Zhi Wang, 6-Nov-2025.)
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → ∩ 𝑥 ∈ 𝐴 𝐵 = 𝐶)
21.49.4  ZF Set Theory - add the Axiom of Replacement
21.49.4.1  Theorems requiring subset and intersection existence
Theorem	inpw 49329*	Two ways of expressing a collection of subsets as seen in df-ntr 23007, unimax 4878, and others. (Contributed by Zhi Wang, 27-Sep-2024.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∩ 𝒫 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝐵})
21.49.5  ZF Set Theory - add the Axiom of Power Sets
21.49.5.1  Ordered pair theorem
Theorem	opth1neg 49330	Two ordered pairs are not equal if their first components are not equal. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≠ 𝐶 → ⟨𝐴, 𝐵⟩ ≠ ⟨𝐶, 𝐷⟩))
Theorem	opth2neg 49331	Two ordered pairs are not equal if their second components are not equal. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ≠ 𝐷 → ⟨𝐴, 𝐵⟩ ≠ ⟨𝐶, 𝐷⟩))
21.49.5.2  Ordered-pair class abstractions (cont.)
Theorem	brab2dd 49332*	Expressing that two sets are related by a binary relation which is expressed as a class abstraction of ordered pairs. (Contributed by Zhi Wang, 24-Sep-2025.)
⊢ (𝜑 → 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜓)})    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ↔ (𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉)))    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ 𝜒)))
Theorem	brab2ddw 49333*	Expressing that two sets are related by a binary relation which is expressed as a class abstraction of ordered pairs. (Contributed by Zhi Wang, 24-Sep-2025.)
⊢ (𝜑 → 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜓)})    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑦 = 𝐵 → (𝜃 ↔ 𝜒))    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝐶 = 𝑈)    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝐷 = 𝑉)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ 𝜒)))
Theorem	brab2ddw2 49334*	Expressing that two sets are related by a binary relation which is expressed as a class abstraction of ordered pairs. (Contributed by Zhi Wang, 24-Sep-2025.)
⊢ (𝜑 → 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜓)})    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑦 = 𝐵 → (𝜃 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐴 → 𝐶 = 𝑈)    &   ⊢ (𝑦 = 𝐵 → 𝐷 = 𝑉)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ 𝜒)))
21.49.5.3  Relations
Theorem	iinxp 49335*	Indexed intersection of Cartesian products is the Cartesian product of indexed intersections. See also inxp 5777 and intxp 49336. (Contributed by Zhi Wang, 30-Oct-2025.)
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (𝐵 × 𝐶) = (∩ 𝑥 ∈ 𝐴 𝐵 × ∩ 𝑥 ∈ 𝐴 𝐶))
Theorem	intxp 49336*	Intersection of Cartesian products is the Cartesian product of intersection of domains and ranges. See also inxp 5777 and iinxp 49335. (Contributed by Zhi Wang, 30-Oct-2025.)
⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 = (dom 𝑥 × ran 𝑥))    &   ⊢ 𝑋 = ∩ 𝑥 ∈ 𝐴 dom 𝑥    &   ⊢ 𝑌 = ∩ 𝑥 ∈ 𝐴 ran 𝑥    ⇒   ⊢ (𝜑 → ∩ 𝐴 = (𝑋 × 𝑌))
Theorem	coxp 49337	Composition with a Cartesian product. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (𝐴 ∘ (𝐵 × 𝐶)) = (𝐵 × (𝐴 “ 𝐶))
Theorem	cosn 49338	Composition with an ordered pair singleton. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ ((𝐵 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) → (𝐴 ∘ {⟨𝐵, 𝐶⟩}) = ({𝐵} × (𝐴 “ {𝐶})))
Theorem	cosni 49339	Composition with an ordered pair singleton. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴 ∘ {⟨𝐵, 𝐶⟩}) = ({𝐵} × (𝐴 “ {𝐶}))
Theorem	inisegn0a 49340	The inverse image of a singleton subset of an image is non-empty. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ (𝐴 ∈ (𝐹 “ 𝐵) → (◡𝐹 “ {𝐴}) ≠ ∅)
Theorem	dmrnxp 49341	A Cartesian product is the Cartesian product of its domain and range. (Contributed by Zhi Wang, 30-Oct-2025.)
⊢ (𝑅 = (𝐴 × 𝐵) → 𝑅 = (dom 𝑅 × ran 𝑅))
21.49.5.4  Functions
Theorem	mof0 49342	There is at most one function into the empty set. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ ∃*𝑓 𝑓:𝐴⟶∅
Theorem	mof02 49343*	A variant of mof0 49342. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝐵 = ∅ → ∃*𝑓 𝑓:𝐴⟶𝐵)
Theorem	mof0ALT 49344*	Alternate proof of mof0 49342 with stronger requirements on distinct variables. Uses mo4 2572. (Contributed by Zhi Wang, 19-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃*𝑓 𝑓:𝐴⟶∅
Theorem	eufsnlem 49345*	There is exactly one function into a singleton. For a simpler hypothesis, see eufsn 49346 assuming ax-rep 5202, or eufsn2 49347 assuming ax-pow 5297 and ax-un 7682. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → (𝐴 × {𝐵}) ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃!𝑓 𝑓:𝐴⟶{𝐵})
Theorem	eufsn 49346*	There is exactly one function into a singleton, assuming ax-rep 5202. See eufsn2 49347 for different axiom requirements. If existence is not needed, use mofsn 49348 or mofsn2 49349 for fewer axiom assumptions. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃!𝑓 𝑓:𝐴⟶{𝐵})
Theorem	eufsn2 49347*	There is exactly one function into a singleton, assuming ax-pow 5297 and ax-un 7682. Variant of eufsn 49346. If existence is not needed, use mofsn 49348 or mofsn2 49349 for fewer axiom assumptions. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃!𝑓 𝑓:𝐴⟶{𝐵})
Theorem	mofsn 49348*	There is at most one function into a singleton, with fewer axioms than eufsn 49346 and eufsn2 49347. See also mofsn2 49349. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ (𝐵 ∈ 𝑉 → ∃*𝑓 𝑓:𝐴⟶{𝐵})
Theorem	mofsn2 49349*	There is at most one function into a singleton. An unconditional variant of mofsn 49348, i.e., the singleton could be empty if 𝑌 is a proper class. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ (𝐵 = {𝑌} → ∃*𝑓 𝑓:𝐴⟶𝐵)
Theorem	mofsssn 49350*	There is at most one function into a subclass of a singleton. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝐵 ⊆ {𝑌} → ∃*𝑓 𝑓:𝐴⟶𝐵)
Theorem	mofmo 49351*	There is at most one function into a class containing at most one element. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ (∃*𝑥 𝑥 ∈ 𝐵 → ∃*𝑓 𝑓:𝐴⟶𝐵)
Theorem	mofeu 49352*	The uniqueness of a function into a set with at most one element. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ 𝐺 = (𝐴 × 𝐵)    &   ⊢ (𝜑 → (𝐵 = ∅ → 𝐴 = ∅))    &   ⊢ (𝜑 → ∃*𝑥 𝑥 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐹 = 𝐺))
Theorem	elfvne0 49353	If a function value has a member, then the function is not an empty set (An artifact of our function value definition.) (Contributed by Zhi Wang, 16-Sep-2024.)
⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐹 ≠ ∅)
Theorem	fdomne0 49354	A function with non-empty domain is non-empty and has non-empty codomain. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ ((𝐹:𝑋⟶𝑌 ∧ 𝑋 ≠ ∅) → (𝐹 ≠ ∅ ∧ 𝑌 ≠ ∅))
Theorem	f1sn2g 49355	A function that maps a singleton to a class is injective. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:{𝐴}⟶𝐵) → 𝐹:{𝐴}–1-1→𝐵)
Theorem	f102g 49356	A function that maps the empty set to a class is injective. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ ((𝐴 = ∅ ∧ 𝐹:𝐴⟶𝐵) → 𝐹:𝐴–1-1→𝐵)
Theorem	f1mo 49357*	A function that maps a set with at most one element to a class is injective. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ ((∃*𝑥 𝑥 ∈ 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝐹:𝐴–1-1→𝐵)
Theorem	f002 49358	A function with an empty codomain must have empty domain. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → (𝐵 = ∅ → 𝐴 = ∅))
Theorem	map0cor 49359*	A function exists iff an empty codomain is accompanied with an empty domain. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ((𝐵 = ∅ → 𝐴 = ∅) ↔ ∃𝑓 𝑓:𝐴⟶𝐵))
Theorem	ffvbr 49360	Relation with function value. (Contributed by Zhi Wang, 25-Nov-2025.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑋 ∈ 𝐴) → 𝑋𝐹(𝐹‘𝑋))
Theorem	xpco2 49361	Composition of a Cartesian product with a function. (Contributed by Zhi Wang, 25-Nov-2025.)
⊢ (𝐹:𝐴⟶𝐵 → ((𝐵 × 𝐶) ∘ 𝐹) = (𝐴 × 𝐶))
21.49.5.5  Operations
Theorem	ovsng 49362	The operation value of a singleton of a nested ordered pair is the last member. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ (𝐶 ∈ 𝑉 → (𝐴{⟨⟨𝐴, 𝐵⟩, 𝐶⟩}𝐵) = 𝐶)
Theorem	ovsng2 49363	The operation value of a singleton of an ordered triple is the last member. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ (𝐶 ∈ 𝑉 → (𝐴{⟨𝐴, 𝐵, 𝐶⟩}𝐵) = 𝐶)
Theorem	ovsn 49364	The operation value of a singleton of a nested ordered pair is the last member. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴{⟨⟨𝐴, 𝐵⟩, 𝐶⟩}𝐵) = 𝐶
Theorem	ovsn2 49365	The operation value of a singleton of an ordered triple is the last member. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴{⟨𝐴, 𝐵, 𝐶⟩}𝐵) = 𝐶
Theorem	fvconstr 49366	Two ways of expressing 𝐴𝑅𝐵. (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ (𝜑 → 𝐹 = (𝑅 × {𝑌}))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ≠ ∅)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐵) = 𝑌))
Theorem	fvconstrn0 49367	Two ways of expressing 𝐴𝑅𝐵. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐹 = (𝑅 × {𝑌}))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ≠ ∅)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐵) ≠ ∅))
Theorem	fvconstr2 49368	Two ways of expressing 𝐴𝑅𝐵. (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ (𝜑 → 𝐹 = (𝑅 × {𝑌}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐴𝐹𝐵))    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐵)
Theorem	ovmpt4d 49369*	Deduction version of ovmpt4g 7507. (This is the operation analogue of fvmpt2d 6953.) (Contributed by Zhi Wang, 9-Oct-2025.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝑉)    ⇒   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐹𝑦) = 𝐶)
Theorem	eqfnovd 49370*	Deduction for equality of operations. (Contributed by Zhi Wang, 19-Nov-2025.)
⊢ (𝜑 → 𝐹 Fn (𝐴 × 𝐵))    &   ⊢ (𝜑 → 𝐺 Fn (𝐴 × 𝐵))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
21.49.6  ZF Set Theory - add the Axiom of Union
21.49.6.1  Relations and functions (cont.)
Theorem	fonex 49371	The domain of a surjection is a proper class if the range is a proper class as well. Can be used to prove that if a structure component extractor restricted to a class maps onto a proper class, then the class is a proper class as well. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ 𝐵 ∉ V    &   ⊢ 𝐹:𝐴–onto→𝐵    ⇒   ⊢ 𝐴 ∉ V
21.49.6.2  First and second members of an ordered pair
Theorem	eloprab1st2nd 49372*	Reconstruction of a nested ordered pair in terms of its ordered pair components. (Contributed by Zhi Wang, 27-Oct-2025.)
⊢ (𝐴 ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} → 𝐴 = ⟨⟨(1st ‘(1st ‘𝐴)), (2nd ‘(1st ‘𝐴))⟩, (2nd ‘𝐴)⟩)
21.49.6.3  Operations in maps-to notation (continued)
Theorem	fmpodg 49373*	Domain and codomain of the mapping operation; deduction form. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑅 = (𝐴 × 𝐵))    ⇒   ⊢ (𝜑 → 𝐹:𝑅⟶𝑆)
Theorem	fmpod 49374*	Domain and codomain of the mapping operation; deduction form. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝐹:(𝐴 × 𝐵)⟶𝑆)
21.49.6.4  Function transposition
Theorem	resinsnlem 49375	Lemma for resinsnALT 49377. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (𝜑 → (𝜒 ↔ ¬ 𝜓))    &   ⊢ (¬ 𝜑 → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ 𝜒)
Theorem	resinsn 49376	Restriction to the intersection with a singleton. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ ((𝐹 ↾ (𝐴 ∩ {𝐵})) = ∅ ↔ ¬ 𝐵 ∈ (dom 𝐹 ∩ 𝐴))
Theorem	resinsnALT 49377	Restriction to the intersection with a singleton. (Contributed by Zhi Wang, 6-Oct-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐹 ↾ (𝐴 ∩ {𝐵})) = ∅ ↔ ¬ 𝐵 ∈ (dom 𝐹 ∩ 𝐴))
Theorem	dftpos5 49378*	Alternate definition of tpos. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ tpos 𝐹 = (𝐹 ∘ ((𝑥 ∈ ◡dom 𝐹 ↦ ∪ ◡{𝑥}) ∪ {⟨∅, ∅⟩}))
Theorem	dftpos6 49379*	Alternate definition of tpos. The second half of the right hand side could apply ressn 6240 and become (𝐹 ↾ {∅}). (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ tpos 𝐹 = ((𝐹 ∘ (𝑥 ∈ ◡dom 𝐹 ↦ ∪ ◡{𝑥})) ∪ ({∅} × (𝐹 “ {∅})))
Theorem	dmtposss 49380	The domain of tpos 𝐹 is a subset. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ dom tpos 𝐹 ⊆ ((V × V) ∪ {∅})
Theorem	tposres0 49381	The transposition of a set restricted to the empty set is the set restricted to the empty set. See also ressn 6240 and dftpos6 49379 for an alternate proof. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (tpos 𝐹 ↾ {∅}) = (𝐹 ↾ {∅})
Theorem	tposresg 49382	The transposition restricted to a set. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (tpos 𝐹 ↾ 𝑅) = ((tpos 𝐹 ↾ ◡◡𝑅) ∪ (𝐹 ↾ (𝑅 ∩ {∅})))
Theorem	tposrescnv 49383*	The transposition restricted to a converse is the transposition of the restricted class, with the empty set removed from the domain. Note that the right hand side is a more useful form of (tpos (𝐹 ↾ 𝑅) ↾ (V ∖ {∅})) by df-tpos 8170. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (tpos 𝐹 ↾ ◡𝑅) = (𝐹 ∘ (𝑥 ∈ ◡dom (𝐹 ↾ 𝑅) ↦ ∪ ◡{𝑥}))
Theorem	tposres2 49384	The transposition restricted to a set. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (𝜑 → ¬ ∅ ∈ (dom 𝐹 ∩ 𝑅))    ⇒   ⊢ (𝜑 → (tpos 𝐹 ↾ 𝑅) = (tpos 𝐹 ↾ ◡◡𝑅))
Theorem	tposres3 49385	The transposition restricted to a set. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (𝜑 → ¬ ∅ ∈ (dom 𝐹 ∩ 𝑅))    ⇒   ⊢ (𝜑 → (tpos 𝐹 ↾ 𝑅) = tpos (𝐹 ↾ ◡𝑅))
Theorem	tposres 49386	The transposition restricted to a relation. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (Rel 𝑅 → (tpos 𝐹 ↾ 𝑅) = tpos (𝐹 ↾ ◡𝑅))
Theorem	tposresxp 49387	The transposition restricted to a Cartesian product. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (tpos 𝐹 ↾ (𝐴 × 𝐵)) = tpos (𝐹 ↾ (𝐵 × 𝐴))
Theorem	tposf1o 49388	Condition of a bijective transposition. (Contributed by Zhi Wang, 5-Oct-2025.)
⊢ (𝐹:(𝐴 × 𝐵)–1-1-onto→𝐶 → tpos 𝐹:(𝐵 × 𝐴)–1-1-onto→𝐶)
Theorem	tposid 49389	Swap an ordered pair. (Contributed by Zhi Wang, 5-Oct-2025.)
⊢ (𝑋tpos I 𝑌) = ⟨𝑌, 𝑋⟩
Theorem	tposidres 49390	Swap an ordered pair. (Contributed by Zhi Wang, 5-Oct-2025.)
⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑌tpos ( I ↾ (𝐴 × 𝐵))𝑋) = ⟨𝑋, 𝑌⟩)
Theorem	tposidf1o 49391	The swap function, or the twisting map, is bijective. (Contributed by Zhi Wang, 5-Oct-2025.)
⊢ tpos ( I ↾ (𝐴 × 𝐵)):(𝐵 × 𝐴)–1-1-onto→(𝐴 × 𝐵)
Theorem	tposideq 49392*	Two ways of expressing the swap function. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (Rel 𝑅 → (tpos I ↾ 𝑅) = (𝑥 ∈ 𝑅 ↦ ∪ ◡{𝑥}))
Theorem	tposideq2 49393*	Two ways of expressing the swap function. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ 𝑅 = (𝐴 × 𝐵)    ⇒   ⊢ (tpos I ↾ 𝑅) = (𝑥 ∈ 𝑅 ↦ ∪ ◡{𝑥})
21.49.6.5  Infinite Cartesian products
Theorem	ixpv 49394*	Infinite Cartesian product of the universal class is the set of functions with a fixed domain. (Contributed by Zhi Wang, 1-Nov-2025.)
⊢ X𝑥 ∈ 𝐴 V = {𝑓 ∣ 𝑓 Fn 𝐴}
21.49.6.6  Equinumerosity
Theorem	fvconst0ci 49395	A constant function's value is either the constant or the empty set. (An artifact of our function value definition.) (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ 𝐵 ∈ V    &   ⊢ 𝑌 = ((𝐴 × {𝐵})‘𝑋)    ⇒   ⊢ (𝑌 = ∅ ∨ 𝑌 = 𝐵)
Theorem	fvconstdomi 49396	A constant function's value is dominated by the constant. (An artifact of our function value definition.) (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝐴 × {𝐵})‘𝑋) ≼ 𝐵
Theorem	f1omo 49397*	There is at most one element in the function value of a constant function whose output is 1o. (An artifact of our function value definition.) Proof could be significantly shortened by fvconstdomi 49396 assuming ax-un 7682 (see f1omoALT 49399). (Contributed by Zhi Wang, 19-Sep-2024.) (Proof shortened by SN, 24-Nov-2025.)
⊢ (𝜑 → 𝐹 = (𝐴 × {1o}))    ⇒   ⊢ (𝜑 → ∃*𝑦 𝑦 ∈ (𝐹‘𝑋))
Theorem	f1omoOLD 49398*	Obsolete version of f1omo 49397 as of 24-Nov-2025. (Contributed by Zhi Wang, 19-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐹 = (𝐴 × {1o}))    ⇒   ⊢ (𝜑 → ∃*𝑦 𝑦 ∈ (𝐹‘𝑋))
Theorem	f1omoALT 49399*	There is at most one element in the function value of a constant function whose output is 1o. (An artifact of our function value definition.) Use f1omo 49397 without assuming ax-un 7682. (Contributed by Zhi Wang, 18-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐹 = (𝐴 × {1o}))    ⇒   ⊢ (𝜑 → ∃*𝑦 𝑦 ∈ (𝐹‘𝑋))
21.49.7  Order sets
21.49.7.1  Real number intervals
Theorem	iccin 49400	Intersection of two closed intervals of extended reals. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴[,]𝐵) ∩ (𝐶[,]𝐷)) = (if(𝐴 ≤ 𝐶, 𝐶, 𝐴)[,]if(𝐵 ≤ 𝐷, 𝐵, 𝐷)))