P. 495 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49401-49500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	2itscplem2 49401	Lemma 2 for 2itscp 49403. (Contributed by AV, 4-Mar-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ 𝐷 = (𝑋 − 𝐴)    &   ⊢ 𝐸 = (𝐵 − 𝑌)    &   ⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴))    ⇒   ⊢ (𝜑 → (𝐶↑2) = ((((𝐷↑2) · (𝐵↑2)) + (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))) + ((𝐸↑2) · (𝐴↑2))))
Theorem	2itscplem3 49402	Lemma D for 2itscp 49403. (Contributed by AV, 4-Mar-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ 𝐷 = (𝑋 − 𝐴)    &   ⊢ 𝐸 = (𝐵 − 𝑌)    &   ⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ 𝑄 = ((𝐸↑2) + (𝐷↑2))    &   ⊢ 𝑆 = (((𝑅↑2) · 𝑄) − (𝐶↑2))    ⇒   ⊢ (𝜑 → 𝑆 = ((((𝐸↑2) · ((𝑅↑2) − (𝐴↑2))) + ((𝐷↑2) · ((𝑅↑2) − (𝐵↑2)))) − (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))))
Theorem	2itscp 49403	A condition for a quadratic equation with real coefficients (for the intersection points of a line with a circle) to have (exactly) two different real solutions. (Contributed by AV, 5-Mar-2023.) (Revised by AV, 16-May-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ 𝐷 = (𝑋 − 𝐴)    &   ⊢ 𝐸 = (𝐵 − 𝑌)    &   ⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) < (𝑅↑2))    &   ⊢ (𝜑 → (𝐵 ≠ 𝑌 ∨ 𝐴 ≠ 𝑋))    &   ⊢ 𝑄 = ((𝐸↑2) + (𝐷↑2))    &   ⊢ 𝑆 = (((𝑅↑2) · 𝑄) − (𝐶↑2))    ⇒   ⊢ (𝜑 → 0 < 𝑆)
Theorem	itscnhlinecirc02plem1 49404	Lemma 1 for itscnhlinecirc02p 49407. (Contributed by AV, 6-Mar-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ 𝐷 = (𝑋 − 𝐴)    &   ⊢ 𝐸 = (𝐵 − 𝑌)    &   ⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) < (𝑅↑2))    &   ⊢ (𝜑 → 𝐵 ≠ 𝑌)    ⇒   ⊢ (𝜑 → 0 < ((-(2 · (𝐷 · 𝐶))↑2) − (4 · (((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2)))))))
Theorem	itscnhlinecirc02plem2 49405	Lemma 2 for itscnhlinecirc02p 49407. (Contributed by AV, 10-Mar-2023.)
⊢ 𝐷 = (𝑋 − 𝐴)    &   ⊢ 𝐸 = (𝐵 − 𝑌)    &   ⊢ 𝐶 = ((𝐵 · 𝑋) − (𝐴 · 𝑌))    ⇒   ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) ∧ 𝐵 ≠ 𝑌) ∧ (𝑅 ∈ ℝ ∧ ((𝐴↑2) + (𝐵↑2)) < (𝑅↑2))) → 0 < ((-(2 · (𝐷 · 𝐶))↑2) − (4 · (((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2)))))))
Theorem	itscnhlinecirc02plem3 49406	Lemma 3 for itscnhlinecirc02p 49407. (Contributed by AV, 10-Mar-2023.)
⊢ 𝐼 = {1, 2}    &   ⊢ 𝐸 = (ℝ^‘𝐼)    &   ⊢ 𝑃 = (ℝ ↑m 𝐼)    &   ⊢ 𝑆 = (Sphere‘𝐸)    &   ⊢ 0 = (𝐼 × {0})    &   ⊢ 𝐿 = (LineM‘𝐸)    &   ⊢ 𝐷 = (dist‘𝐸)    ⇒   ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → 0 < ((-(2 · (((𝑌‘1) − (𝑋‘1)) · (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))))↑2) − (4 · (((((𝑋‘2) − (𝑌‘2))↑2) + (((𝑌‘1) − (𝑋‘1))↑2)) · (((((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))↑2) − ((((𝑋‘2) − (𝑌‘2))↑2) · (𝑅↑2)))))))
Theorem	itscnhlinecirc02p 49407*	Intersection of a nonhorizontal line with a circle: A nonhorizontal line passing through a point within a circle around the origin intersects the circle at exactly two different points. (Contributed by AV, 28-Jan-2023.)
⊢ 𝐼 = {1, 2}    &   ⊢ 𝐸 = (ℝ^‘𝐼)    &   ⊢ 𝑃 = (ℝ ↑m 𝐼)    &   ⊢ 𝑆 = (Sphere‘𝐸)    &   ⊢ 0 = (𝐼 × {0})    &   ⊢ 𝐿 = (LineM‘𝐸)    &   ⊢ 𝐷 = (dist‘𝐸)    &   ⊢ 𝑍 = {⟨1, 𝑥⟩, ⟨2, 𝑦⟩}    ⇒   ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → ∃!𝑠 ∈ 𝒫 ℝ((♯‘𝑠) = 2 ∧ ∀𝑦 ∈ 𝑠 ∃!𝑥 ∈ ℝ (𝑍 ∈ ( 0 𝑆𝑅) ∧ 𝑍 ∈ (𝑋𝐿𝑌))))
Theorem	inlinecirc02plem 49408*	Lemma for inlinecirc02p 49409. (Contributed by AV, 7-May-2023.) (Revised by AV, 15-May-2023.)
⊢ 𝐼 = {1, 2}    &   ⊢ 𝐸 = (ℝ^‘𝐼)    &   ⊢ 𝑃 = (ℝ ↑m 𝐼)    &   ⊢ 𝑆 = (Sphere‘𝐸)    &   ⊢ 0 = (𝐼 × {0})    &   ⊢ 𝐿 = (LineM‘𝐸)    &   ⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2))    &   ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2))    &   ⊢ 𝐴 = ((𝑋‘2) − (𝑌‘2))    &   ⊢ 𝐵 = ((𝑌‘1) − (𝑋‘1))    &   ⊢ 𝐶 = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))    ⇒   ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏))
Theorem	inlinecirc02p 49409	Intersection of a line with a circle: A line passing through a point within a circle around the origin intersects the circle at exactly two different points. (Contributed by AV, 9-May-2023.) (Revised by AV, 16-May-2023.)
⊢ 𝐼 = {1, 2}    &   ⊢ 𝐸 = (ℝ^‘𝐼)    &   ⊢ 𝑃 = (ℝ ↑m 𝐼)    &   ⊢ 𝑆 = (Sphere‘𝐸)    &   ⊢ 0 = (𝐼 × {0})    &   ⊢ 𝐿 = (LineM‘𝐸)    &   ⊢ 𝐷 = (dist‘𝐸)    ⇒   ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → (( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) ∈ (Pairsproper‘𝑃))
Theorem	inlinecirc02preu 49410*	Intersection of a line with a circle: A line passing through a point within a circle around the origin intersects the circle at exactly two different points, expressed with restricted uniqueness (and without the definition of proper pairs). (Contributed by AV, 16-May-2023.)
⊢ 𝐼 = {1, 2}    &   ⊢ 𝐸 = (ℝ^‘𝐼)    &   ⊢ 𝑃 = (ℝ ↑m 𝐼)    &   ⊢ 𝑆 = (Sphere‘𝐸)    &   ⊢ 0 = (𝐼 × {0})    &   ⊢ 𝐿 = (LineM‘𝐸)    &   ⊢ 𝐷 = (dist‘𝐸)    ⇒   ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → ∃!𝑝 ∈ 𝒫 𝑃((♯‘𝑝) = 2 ∧ 𝑝 = (( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌))))
21.49  Mathbox for Zhi Wang
21.49.1  Propositional calculus
Theorem	pm4.71da 49411	Deduction converting a biconditional to a biconditional with conjunction. Variant of pm4.71d 569. (Contributed by Zhi Wang, 30-Aug-2024.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒)))
Theorem	logic1 49412	Distribution of implication over biconditional with replacement (deduction form). (Contributed by Zhi Wang, 30-Aug-2024.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜓 → (𝜃 ↔ 𝜏)))    ⇒   ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏)))
Theorem	logic1a 49413	Variant of logic1 49412. (Contributed by Zhi Wang, 30-Aug-2024.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝜓) → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏)))
Theorem	logic2 49414	Variant of logic1 49412. (Contributed by Zhi Wang, 30-Aug-2024.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)))    ⇒   ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏)))
Theorem	pm5.32dav 49415	Distribution of implication over biconditional (deduction form). Variant of pm5.32da 587. (Contributed by Zhi Wang, 30-Aug-2024.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))    ⇒   ⊢ (𝜑 → ((𝜒 ∧ 𝜓) ↔ (𝜃 ∧ 𝜓)))
Theorem	pm5.32dra 49416	Reverse distribution of implication over biconditional (deduction form). (Contributed by Zhi Wang, 6-Sep-2024.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))
Theorem	exp12bd 49417	The import-export theorem (impexp 454) for biconditionals (deduction form). (Contributed by Zhi Wang, 3-Sep-2024.)
⊢ (𝜑 → (((𝜓 ∧ 𝜒) → 𝜃) ↔ ((𝜏 ∧ 𝜂) → 𝜁)))    ⇒   ⊢ (𝜑 → ((𝜓 → (𝜒 → 𝜃)) ↔ (𝜏 → (𝜂 → 𝜁))))
Theorem	mpbiran3d 49418	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 49419	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 49420*	An example of how ax-5 1930 without a distinct variable condition causes paradox in models of at least two objects. The hypothesis "dtrucor3.1" is provable from dtru 5404 in the ZF set theory. axc16nf 2298 and euae 2686 demonstrate that the violation of dtru 5404 leads to a model with only one object assuming its existence (ax-6 1987). The conclusion is also provable in the empty model ( see emptyal 1928). See also nf5 2316 and nf5i 2180 for the relation between unconditional ax-5 1930 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 49421*	Formula-building rule for restricted universal quantifier and additional condition (deduction form). See ralbidc 49422 for a more generalized form. (Contributed by Zhi Wang, 6-Sep-2024.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜓)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜒 ↔ 𝜃))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜒 ↔ ∀𝑥 ∈ 𝐵 (𝜓 → 𝜃)))
Theorem	ralbidc 49422*	Formula-building rule for restricted universal quantifier and additional condition (deduction form). A variant of ralbidb 49421. (Contributed by Zhi Wang, 30-Aug-2024.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜓)))    &   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) → (𝜒 ↔ 𝜃)))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜒 ↔ ∀𝑥 ∈ 𝐵 (𝜓 → 𝜃)))
Theorem	r19.41dv 49423*	A complex deduction form of r19.41v 3192. (Contributed by Zhi Wang, 6-Sep-2024.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒))
Theorem	rmotru 49424	Two ways of expressing "at most one" element. (Contributed by Zhi Wang, 19-Sep-2024.) (Proof shortened by BJ, 23-Sep-2024.)
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∃*𝑥 ∈ 𝐴 ⊤)
Theorem	reutru 49425	Two ways of expressing "exactly one" element. (Contributed by Zhi Wang, 23-Sep-2024.)
⊢ (∃!𝑥 𝑥 ∈ 𝐴 ↔ ∃!𝑥 ∈ 𝐴 ⊤)
Theorem	reutruALT 49426	Alternate proof of reutru 49425. (Contributed by Zhi Wang, 23-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃!𝑥 𝑥 ∈ 𝐴 ↔ ∃!𝑥 ∈ 𝐴 ⊤)
Theorem	reueqbidva 49427*	Formula-building rule for restricted existential uniqueness quantifier. Deduction form. General version of reueqbidv 3403. (Contributed by Zhi Wang, 20-Nov-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐵 𝜒))
21.49.3.2  The universal class
Theorem	reuxfr1dd 49428*	Transfer existential uniqueness from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. Simplifies reuxfr1d 3713. (Contributed by Zhi Wang, 20-Sep-2025.)
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃!𝑦 ∈ 𝐶 𝑥 = 𝐴)    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐴)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 𝜓 ↔ ∃!𝑦 ∈ 𝐶 𝜒))
21.49.3.3  The empty set
Theorem	ssdisjd 49429	Subset preserves disjointness. Deduction form of ssdisj 4414. (Contributed by Zhi Wang, 7-Sep-2024.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → (𝐵 ∩ 𝐶) = ∅)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐶) = ∅)
Theorem	ssdisjdr 49430	Subset preserves disjointness. Deduction form of ssdisj 4414. Alternatively this could be proved with ineqcom 4162 in tandem with ssdisjd 49429. (Contributed by Zhi Wang, 7-Sep-2024.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → (𝐶 ∩ 𝐵) = ∅)    ⇒   ⊢ (𝜑 → (𝐶 ∩ 𝐴) = ∅)
Theorem	disjdifb 49431	Relative complement is anticommutative regarding intersection. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ ((𝐴 ∖ 𝐵) ∩ (𝐵 ∖ 𝐴)) = ∅
Theorem	predisj 49432	Preimages of disjoint sets are disjoint. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → 𝑆 ⊆ (◡𝐹 “ 𝐴))    &   ⊢ (𝜑 → 𝑇 ⊆ (◡𝐹 “ 𝐵))    ⇒   ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅)
21.49.3.4  Unordered and ordered pairs
Theorem	vsn 49433	The singleton of the universal class is the empty set. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ {V} = ∅
Theorem	mosn 49434*	"At most one" element in a singleton. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ (𝐴 = {𝐵} → ∃*𝑥 𝑥 ∈ 𝐴)
Theorem	mo0 49435*	"At most one" element in an empty set. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ (𝐴 = ∅ → ∃*𝑥 𝑥 ∈ 𝐴)
Theorem	mosssn 49436*	"At most one" element in a subclass of a singleton. (Contributed by Zhi Wang, 23-Sep-2024.)
⊢ (𝐴 ⊆ {𝐵} → ∃*𝑥 𝑥 ∈ 𝐴)
Theorem	mo0sn 49437*	Two ways of expressing "at most one" element in a class. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ (𝐴 = ∅ ∨ ∃𝑦 𝐴 = {𝑦}))
Theorem	mosssn2 49438*	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 49439*	Superclass of the greatest lower bound. A dual statement of ssintub 4924. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴} ⊆ 𝐴
21.49.3.6  Indexed union and intersection
Theorem	iuneq0 49440	An indexed union is empty iff all indexed classes are empty. (Contributed by Zhi Wang, 1-Nov-2025.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 = ∅ ↔ ∪ 𝑥 ∈ 𝐴 𝐵 = ∅)
Theorem	iineq0 49441	An indexed intersection is empty if one of the intersected classes is empty. (Contributed by Zhi Wang, 30-Oct-2025.)
⊢ (∃𝑥 ∈ 𝐴 𝐵 = ∅ → ∩ 𝑥 ∈ 𝐴 𝐵 = ∅)
Theorem	iunlub 49442*	The indexed union is the the lowest upper bound if it exists. (Contributed by Zhi Wang, 1-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = 𝐶)
Theorem	iinglb 49443*	The indexed intersection is the the greatest lower bound if it exists. (Contributed by Zhi Wang, 1-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 = 𝐶)
Theorem	iuneqconst2 49444*	Indexed union of identical classes. (Contributed by Zhi Wang, 6-Nov-2025.)
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → ∪ 𝑥 ∈ 𝐴 𝐵 = 𝐶)
Theorem	iineqconst2 49445*	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 49446*	Two ways of expressing a collection of subsets as seen in df-ntr 23080, unimax 4903, 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 49447	Two ordered pairs are not equal if their first components are not equal. (Contributed by Zhi Wang, 7-Oct-2025.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≠ 𝐶 → ⟨𝐴, 𝐵⟩ ≠ ⟨𝐶, 𝐷⟩))
Theorem	opth2neg 49448	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 49449*	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 49450*	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 49451*	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 49452*	Indexed intersection of Cartesian products is the Cartesian product of indexed intersections. See also inxp 5804 and intxp 49453. (Contributed by Zhi Wang, 30-Oct-2025.)
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (𝐵 × 𝐶) = (∩ 𝑥 ∈ 𝐴 𝐵 × ∩ 𝑥 ∈ 𝐴 𝐶))
Theorem	intxp 49453*	Intersection of Cartesian products is the Cartesian product of intersection of domains and ranges. See also inxp 5804 and iinxp 49452. (Contributed by Zhi Wang, 30-Oct-2025.)
⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 = (dom 𝑥 × ran 𝑥))    &   ⊢ 𝑋 = ∩ 𝑥 ∈ 𝐴 dom 𝑥    &   ⊢ 𝑌 = ∩ 𝑥 ∈ 𝐴 ran 𝑥    ⇒   ⊢ (𝜑 → ∩ 𝐴 = (𝑋 × 𝑌))
Theorem	coxp 49454	Composition with a Cartesian product. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (𝐴 ∘ (𝐵 × 𝐶)) = (𝐵 × (𝐴 “ 𝐶))
Theorem	cosn 49455	Composition with an ordered pair singleton. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ ((𝐵 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) → (𝐴 ∘ {⟨𝐵, 𝐶⟩}) = ({𝐵} × (𝐴 “ {𝐶})))
Theorem	cosni 49456	Composition with an ordered pair singleton. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴 ∘ {⟨𝐵, 𝐶⟩}) = ({𝐵} × (𝐴 “ {𝐶}))
Theorem	inisegn0a 49457	The inverse image of a singleton subset of an image is non-empty. (Contributed by Zhi Wang, 7-Nov-2025.)
⊢ (𝐴 ∈ (𝐹 “ 𝐵) → (◡𝐹 “ {𝐴}) ≠ ∅)
Theorem	dmrnxp 49458	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 49459	There is at most one function into the empty set. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ ∃*𝑓 𝑓:𝐴⟶∅
Theorem	mof02 49460*	A variant of mof0 49459. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝐵 = ∅ → ∃*𝑓 𝑓:𝐴⟶𝐵)
Theorem	mof0ALT 49461*	Alternate proof of mof0 49459 with stronger requirements on distinct variables. Uses mo4 2593. (Contributed by Zhi Wang, 19-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃*𝑓 𝑓:𝐴⟶∅
Theorem	eufsnlem 49462*	There is exactly one function into a singleton. For a simpler hypothesis, see eufsn 49463 assuming ax-rep 5227, or eufsn2 49464 assuming ax-pow 5322 and ax-un 7718. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → (𝐴 × {𝐵}) ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃!𝑓 𝑓:𝐴⟶{𝐵})
Theorem	eufsn 49463*	There is exactly one function into a singleton, assuming ax-rep 5227. See eufsn2 49464 for different axiom requirements. If existence is not needed, use mofsn 49465 or mofsn2 49466 for fewer axiom assumptions. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃!𝑓 𝑓:𝐴⟶{𝐵})
Theorem	eufsn2 49464*	There is exactly one function into a singleton, assuming ax-pow 5322 and ax-un 7718. Variant of eufsn 49463. If existence is not needed, use mofsn 49465 or mofsn2 49466 for fewer axiom assumptions. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃!𝑓 𝑓:𝐴⟶{𝐵})
Theorem	mofsn 49465*	There is at most one function into a singleton, with fewer axioms than eufsn 49463 and eufsn2 49464. See also mofsn2 49466. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ (𝐵 ∈ 𝑉 → ∃*𝑓 𝑓:𝐴⟶{𝐵})
Theorem	mofsn2 49466*	There is at most one function into a singleton. An unconditional variant of mofsn 49465, i.e., the singleton could be empty if 𝑌 is a proper class. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ (𝐵 = {𝑌} → ∃*𝑓 𝑓:𝐴⟶𝐵)
Theorem	mofsssn 49467*	There is at most one function into a subclass of a singleton. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝐵 ⊆ {𝑌} → ∃*𝑓 𝑓:𝐴⟶𝐵)
Theorem	mofmo 49468*	There is at most one function into a class containing at most one element. (Contributed by Zhi Wang, 19-Sep-2024.)
⊢ (∃*𝑥 𝑥 ∈ 𝐵 → ∃*𝑓 𝑓:𝐴⟶𝐵)
Theorem	mofeu 49469*	The uniqueness of a function into a set with at most one element. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ 𝐺 = (𝐴 × 𝐵)    &   ⊢ (𝜑 → (𝐵 = ∅ → 𝐴 = ∅))    &   ⊢ (𝜑 → ∃*𝑥 𝑥 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐹 = 𝐺))
Theorem	elfvne0 49470	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 49471	A function with non-empty domain is non-empty and has non-empty codomain. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ ((𝐹:𝑋⟶𝑌 ∧ 𝑋 ≠ ∅) → (𝐹 ≠ ∅ ∧ 𝑌 ≠ ∅))
Theorem	f1sn2g 49472	A function that maps a singleton to a class is injective. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:{𝐴}⟶𝐵) → 𝐹:{𝐴}–1-1→𝐵)
Theorem	f102g 49473	A function that maps the empty set to a class is injective. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ ((𝐴 = ∅ ∧ 𝐹:𝐴⟶𝐵) → 𝐹:𝐴–1-1→𝐵)
Theorem	f1mo 49474*	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 49475	A function with an empty codomain must have empty domain. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → (𝐵 = ∅ → 𝐴 = ∅))
Theorem	map0cor 49476*	A function exists iff an empty codomain is accompanied with an empty domain. (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ((𝐵 = ∅ → 𝐴 = ∅) ↔ ∃𝑓 𝑓:𝐴⟶𝐵))
Theorem	ffvbr 49477	Relation with function value. (Contributed by Zhi Wang, 25-Nov-2025.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑋 ∈ 𝐴) → 𝑋𝐹(𝐹‘𝑋))
Theorem	xpco2 49478	Composition of a Cartesian product with a function. (Contributed by Zhi Wang, 25-Nov-2025.)
⊢ (𝐹:𝐴⟶𝐵 → ((𝐵 × 𝐶) ∘ 𝐹) = (𝐴 × 𝐶))
21.49.5.5  Operations
Theorem	ovsng 49479	The operation value of a singleton of a nested ordered pair is the last member. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ (𝐶 ∈ 𝑉 → (𝐴{⟨⟨𝐴, 𝐵⟩, 𝐶⟩}𝐵) = 𝐶)
Theorem	ovsng2 49480	The operation value of a singleton of an ordered triple is the last member. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ (𝐶 ∈ 𝑉 → (𝐴{⟨𝐴, 𝐵, 𝐶⟩}𝐵) = 𝐶)
Theorem	ovsn 49481	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 49482	The operation value of a singleton of an ordered triple is the last member. (Contributed by Zhi Wang, 22-Oct-2025.)
⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴{⟨𝐴, 𝐵, 𝐶⟩}𝐵) = 𝐶
Theorem	fvconstr 49483	Two ways of expressing 𝐴𝑅𝐵. (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ (𝜑 → 𝐹 = (𝑅 × {𝑌}))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ≠ ∅)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐵) = 𝑌))
Theorem	fvconstrn0 49484	Two ways of expressing 𝐴𝑅𝐵. (Contributed by Zhi Wang, 20-Sep-2024.)
⊢ (𝜑 → 𝐹 = (𝑅 × {𝑌}))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ≠ ∅)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐵) ≠ ∅))
Theorem	fvconstr2 49485	Two ways of expressing 𝐴𝑅𝐵. (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ (𝜑 → 𝐹 = (𝑅 × {𝑌}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐴𝐹𝐵))    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐵)
Theorem	ovmpt4d 49486*	Deduction version of ovmpt4g 7543. (This is the operation analogue of fvmpt2d 6989.) (Contributed by Zhi Wang, 9-Oct-2025.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝑉)    ⇒   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐹𝑦) = 𝐶)
Theorem	eqfnovd 49487*	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 49488	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 49489*	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 49490*	Domain and codomain of the mapping operation; deduction form. (Contributed by Zhi Wang, 29-Sep-2025.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑅 = (𝐴 × 𝐵))    ⇒   ⊢ (𝜑 → 𝐹:𝑅⟶𝑆)
Theorem	fmpod 49491*	Domain and codomain of the mapping operation; deduction form. (Contributed by Zhi Wang, 30-Sep-2025.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝐹:(𝐴 × 𝐵)⟶𝑆)
21.49.6.4  Function transposition
Theorem	resinsnlem 49492	Lemma for resinsnALT 49494. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (𝜑 → (𝜒 ↔ ¬ 𝜓))    &   ⊢ (¬ 𝜑 → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ 𝜒)
Theorem	resinsn 49493	Restriction to the intersection with a singleton. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ ((𝐹 ↾ (𝐴 ∩ {𝐵})) = ∅ ↔ ¬ 𝐵 ∈ (dom 𝐹 ∩ 𝐴))
Theorem	resinsnALT 49494	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 49495*	Alternate definition of tpos. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ tpos 𝐹 = (𝐹 ∘ ((𝑥 ∈ ◡dom 𝐹 ↦ ∪ ◡{𝑥}) ∪ {⟨∅, ∅⟩}))
Theorem	dftpos6 49496*	Alternate definition of tpos. The second half of the right hand side could apply ressn 6272 and become (𝐹 ↾ {∅}). (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ tpos 𝐹 = ((𝐹 ∘ (𝑥 ∈ ◡dom 𝐹 ↦ ∪ ◡{𝑥})) ∪ ({∅} × (𝐹 “ {∅})))
Theorem	dmtposss 49497	The domain of tpos 𝐹 is a subset. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ dom tpos 𝐹 ⊆ ((V × V) ∪ {∅})
Theorem	tposres0 49498	The transposition of a set restricted to the empty set is the set restricted to the empty set. See also ressn 6272 and dftpos6 49496 for an alternate proof. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (tpos 𝐹 ↾ {∅}) = (𝐹 ↾ {∅})
Theorem	tposresg 49499	The transposition restricted to a set. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (tpos 𝐹 ↾ 𝑅) = ((tpos 𝐹 ↾ ◡◡𝑅) ∪ (𝐹 ↾ (𝑅 ∩ {∅})))
Theorem	tposrescnv 49500*	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 8206. (Contributed by Zhi Wang, 6-Oct-2025.)
⊢ (tpos 𝐹 ↾ ◡𝑅) = (𝐹 ∘ (𝑥 ∈ ◡dom (𝐹 ↾ 𝑅) ↦ ∪ ◡{𝑥}))