P. 310 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 30901-31000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	uniin2 30901*	Union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. (Contributed by Thierry Arnoux, 21-Jun-2020.)
⊢ ∪ 𝑥 ∈ 𝐵 (𝐴 ∩ 𝑥) = (𝐴 ∩ ∪ 𝐵)
Theorem	difuncomp 30902	Express a class difference using unions and class complements. (Contributed by Thierry Arnoux, 21-Jun-2020.)
⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∖ 𝐵) = (𝐶 ∖ ((𝐶 ∖ 𝐴) ∪ 𝐵)))
Theorem	elpwunicl 30903	Closure of a set union with regard to elementhood to a power set. (Contributed by Thierry Arnoux, 21-Jun-2020.) (Proof shortened by BJ, 6-Apr-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝒫 𝒫 𝐵)    ⇒   ⊢ (𝜑 → ∪ 𝐴 ∈ 𝒫 𝐵)
20.3.3.7  Indexed union - misc additions
Theorem	cbviunf 30904*	Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by NM, 26-Mar-2006.) (Revised by Andrew Salmon, 25-Jul-2011.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶
Theorem	iuneq12daf 30905	Equality deduction for indexed union, deduction version. (Contributed by Thierry Arnoux, 13-Mar-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷)
Theorem	iunin1f 30906	Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 4989 to recover Enderton's theorem. (Contributed by NM, 26-Mar-2004.) (Revised by Thierry Arnoux, 2-May-2020.)
⊢ Ⅎ𝑥𝐶    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶)
Theorem	ssiun3 30907*	Subset equivalence for an indexed union. (Contributed by Thierry Arnoux, 17-Oct-2016.)
⊢ (∀𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ↔ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	ssiun2sf 30908	Subset relationship for an indexed union. (Contributed by Thierry Arnoux, 31-Dec-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)    ⇒   ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	iuninc 30909*	The union of an increasing collection of sets is its last element. (Contributed by Thierry Arnoux, 22-Jan-2017.)
⊢ (𝜑 → 𝐹 Fn ℕ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)))    ⇒   ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ∪ 𝑛 ∈ (1...𝑖)(𝐹‘𝑛) = (𝐹‘𝑖))
Theorem	iundifdifd 30910*	The intersection of a set is the complement of the union of the complements. (Contributed by Thierry Arnoux, 19-Dec-2016.)
⊢ (𝐴 ⊆ 𝒫 𝑂 → (𝐴 ≠ ∅ → ∩ 𝐴 = (𝑂 ∖ ∪ 𝑥 ∈ 𝐴 (𝑂 ∖ 𝑥))))
Theorem	iundifdif 30911*	The intersection of a set is the complement of the union of the complements. TODO: shorten using iundifdifd 30910. (Contributed by Thierry Arnoux, 4-Sep-2016.)
⊢ 𝑂 ∈ V    &   ⊢ 𝐴 ⊆ 𝒫 𝑂    ⇒   ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 = (𝑂 ∖ ∪ 𝑥 ∈ 𝐴 (𝑂 ∖ 𝑥)))
Theorem	iunrdx 30912*	Re-index an indexed union. (Contributed by Thierry Arnoux, 6-Apr-2017.)
⊢ (𝜑 → 𝐹:𝐴–onto→𝐶)    &   ⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑥)) → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐶 𝐷)
Theorem	iunpreima 30913*	Preimage of an indexed union. (Contributed by Thierry Arnoux, 27-Mar-2018.)
⊢ (Fun 𝐹 → (◡𝐹 “ ∪ 𝑥 ∈ 𝐴 𝐵) = ∪ 𝑥 ∈ 𝐴 (◡𝐹 “ 𝐵))
Theorem	iunrnmptss 30914*	A subset relation for an indexed union over the range of function expressed as a mapping. (Contributed by Thierry Arnoux, 27-Mar-2018.)
⊢ (𝑦 = 𝐵 → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∪ 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐷)
Theorem	iunxunsn 30915*	Appending a set to an indexed union. (Contributed by Thierry Arnoux, 20-Nov-2023.)
⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑋 ∈ 𝑉 → ∪ 𝑥 ∈ (𝐴 ∪ {𝑋})𝐵 = (∪ 𝑥 ∈ 𝐴 𝐵 ∪ 𝐶))
Theorem	iunxunpr 30916*	Appending two sets to an indexed union. (Contributed by Thierry Arnoux, 20-Nov-2023.)
⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶)    &   ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷)    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ∪ 𝑥 ∈ (𝐴 ∪ {𝑋, 𝑌})𝐵 = (∪ 𝑥 ∈ 𝐴 𝐵 ∪ (𝐶 ∪ 𝐷)))
20.3.3.8  Indexed intersection - misc additions
Theorem	iinabrex 30917*	Rewriting an indexed intersection into an intersection of its image set. (Contributed by Thierry Arnoux, 15-Jun-2024.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})
20.3.3.9  Disjointness - misc additions
Theorem	disjnf 30918*	In case 𝑥 is not free in 𝐵, disjointness is not so interesting since it reduces to cases where 𝐴 is a singleton. (Google Groups discussion with Peter Mazsa.) (Contributed by Thierry Arnoux, 26-Jul-2018.)
⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ (𝐵 = ∅ ∨ ∃*𝑥 𝑥 ∈ 𝐴))
Theorem	cbvdisjf 30919*	Change bound variables in a disjoint collection. (Contributed by Thierry Arnoux, 6-Apr-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶)
Theorem	disjss1f 30920	A subset of a disjoint collection is disjoint. (Contributed by Thierry Arnoux, 6-Apr-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ⊆ 𝐵 → (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐴 𝐶))
Theorem	disjeq1f 30921	Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶))
Theorem	disjxun0 30922*	Simplify a disjoint union. (Contributed by Thierry Arnoux, 27-Nov-2023.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 = ∅)    ⇒   ⊢ (𝜑 → (Disj 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 ↔ Disj 𝑥 ∈ 𝐴 𝐶))
Theorem	disjdifprg 30923*	A trivial partition into a subset and its complement. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → Disj 𝑥 ∈ {(𝐵 ∖ 𝐴), 𝐴}𝑥)
Theorem	disjdifprg2 30924*	A trivial partition of a set into its difference and intersection with another set. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ (𝐴 ∈ 𝑉 → Disj 𝑥 ∈ {(𝐴 ∖ 𝐵), (𝐴 ∩ 𝐵)}𝑥)
Theorem	disji2f 30925*	Property of a disjoint collection: if 𝐵(𝑥) = 𝐶 and 𝐵(𝑌) = 𝐷, and 𝑥 ≠ 𝑌, then 𝐵 and 𝐶 are disjoint. (Contributed by Thierry Arnoux, 30-Dec-2016.)
⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐶)    ⇒   ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ 𝑥 ≠ 𝑌) → (𝐵 ∩ 𝐶) = ∅)
Theorem	disjif 30926*	Property of a disjoint collection: if 𝐵(𝑥) and 𝐵(𝑌) = 𝐷 have a common element 𝑍, then 𝑥 = 𝑌. (Contributed by Thierry Arnoux, 30-Dec-2016.)
⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐶)    ⇒   ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (𝑍 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶)) → 𝑥 = 𝑌)
Theorem	disjorf 30927*	Two ways to say that a collection 𝐵(𝑖) for 𝑖 ∈ 𝐴 is disjoint. (Contributed by Thierry Arnoux, 8-Mar-2017.)
⊢ Ⅎ𝑖𝐴    &   ⊢ Ⅎ𝑗𝐴    &   ⊢ (𝑖 = 𝑗 → 𝐵 = 𝐶)    ⇒   ⊢ (Disj 𝑖 ∈ 𝐴 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅))
Theorem	disjorsf 30928*	Two ways to say that a collection 𝐵(𝑖) for 𝑖 ∈ 𝐴 is disjoint. (Contributed by Thierry Arnoux, 8-Mar-2017.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
Theorem	disjif2 30929*	Property of a disjoint collection: if 𝐵(𝑥) and 𝐵(𝑌) = 𝐷 have a common element 𝑍, then 𝑥 = 𝑌. (Contributed by Thierry Arnoux, 6-Apr-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐶)    ⇒   ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (𝑍 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶)) → 𝑥 = 𝑌)
Theorem	disjabrex 30930*	Rewriting a disjoint collection into a partition of its image set. (Contributed by Thierry Arnoux, 30-Dec-2016.)
⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}𝑦)
Theorem	disjabrexf 30931*	Rewriting a disjoint collection into a partition of its image set. (Contributed by Thierry Arnoux, 30-Dec-2016.) (Revised by Thierry Arnoux, 9-Mar-2017.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}𝑦)
Theorem	disjpreima 30932*	A preimage of a disjoint set is disjoint. (Contributed by Thierry Arnoux, 7-Feb-2017.)
⊢ ((Fun 𝐹 ∧ Disj 𝑥 ∈ 𝐴 𝐵) → Disj 𝑥 ∈ 𝐴 (◡𝐹 “ 𝐵))
Theorem	disjrnmpt 30933*	Rewriting a disjoint collection using the range of a mapping. (Contributed by Thierry Arnoux, 27-May-2020.)
⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦)
Theorem	disjin 30934	If a collection is disjoint, so is the collection of the intersections with a given set. (Contributed by Thierry Arnoux, 14-Feb-2017.)
⊢ (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐵 (𝐶 ∩ 𝐴))
Theorem	disjin2 30935	If a collection is disjoint, so is the collection of the intersections with a given set. (Contributed by Thierry Arnoux, 21-Jun-2020.)
⊢ (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐵 (𝐴 ∩ 𝐶))
Theorem	disjxpin 30936*	Derive a disjunction over a Cartesian product from the disjunctions over its first and second elements. (Contributed by Thierry Arnoux, 9-Mar-2018.)
⊢ (𝑥 = (1st ‘𝑝) → 𝐶 = 𝐸)    &   ⊢ (𝑦 = (2nd ‘𝑝) → 𝐷 = 𝐹)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐶)    &   ⊢ (𝜑 → Disj 𝑦 ∈ 𝐵 𝐷)    ⇒   ⊢ (𝜑 → Disj 𝑝 ∈ (𝐴 × 𝐵)(𝐸 ∩ 𝐹))
Theorem	iundisjf 30937*	Rewrite a countable union as a disjoint union. Cf. iundisj 24721. (Contributed by Thierry Arnoux, 31-Dec-2016.)
⊢ Ⅎ𝑘𝐴    &   ⊢ Ⅎ𝑛𝐵    &   ⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵)    ⇒   ⊢ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ 𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)
Theorem	iundisj2f 30938*	A disjoint union is disjoint. Cf. iundisj2 24722. (Contributed by Thierry Arnoux, 30-Dec-2016.)
⊢ Ⅎ𝑘𝐴    &   ⊢ Ⅎ𝑛𝐵    &   ⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵)    ⇒   ⊢ Disj 𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)
Theorem	disjrdx 30939*	Re-index a disjunct collection statement. (Contributed by Thierry Arnoux, 7-Apr-2017.)
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐶)    &   ⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑥)) → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐶 𝐷))
Theorem	disjex 30940*	Two ways to say that two classes are disjoint (or equal). (Contributed by Thierry Arnoux, 4-Oct-2016.)
⊢ ((∃𝑧(𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → 𝐴 = 𝐵) ↔ (𝐴 = 𝐵 ∨ (𝐴 ∩ 𝐵) = ∅))
Theorem	disjexc 30941*	A variant of disjex 30940, applicable for more generic families. (Contributed by Thierry Arnoux, 4-Oct-2016.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ ((∃𝑧(𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → 𝑥 = 𝑦) → (𝐴 = 𝐵 ∨ (𝐴 ∩ 𝐵) = ∅))
Theorem	disjunsn 30942*	Append an element to a disjoint collection. Similar to ralunsn 4826, gsumunsn 19570, etc. (Contributed by Thierry Arnoux, 28-Mar-2018.)
⊢ (𝑥 = 𝑀 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)))
Theorem	disjun0 30943*	Adding the empty element preserves disjointness. (Contributed by Thierry Arnoux, 30-May-2020.)
⊢ (Disj 𝑥 ∈ 𝐴 𝑥 → Disj 𝑥 ∈ (𝐴 ∪ {∅})𝑥)
Theorem	disjiunel 30944*	A set of elements B of a disjoint set A is disjoint with another element of that set. (Contributed by Thierry Arnoux, 24-May-2020.)
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)    &   ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷)    &   ⊢ (𝜑 → 𝐸 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ (𝐴 ∖ 𝐸))    ⇒   ⊢ (𝜑 → (∪ 𝑥 ∈ 𝐸 𝐵 ∩ 𝐷) = ∅)
Theorem	disjuniel 30945*	A set of elements B of a disjoint set A is disjoint with another element of that set. (Contributed by Thierry Arnoux, 24-May-2020.)
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝑥)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴 ∖ 𝐵))    ⇒   ⊢ (𝜑 → (∪ 𝐵 ∩ 𝐶) = ∅)
20.3.4  Relations and Functions
20.3.4.1  Relations - misc additions
Theorem	xpdisjres 30946	Restriction of a constant function (or other Cartesian product) outside of its domain. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ ((𝐴 ∩ 𝐶) = ∅ → ((𝐴 × 𝐵) ↾ 𝐶) = ∅)
Theorem	opeldifid 30947	Ordered pair elementhood outside of the diagonal. (Contributed by Thierry Arnoux, 1-Jan-2020.)
⊢ (Rel 𝐴 → (⟨𝑋, 𝑌⟩ ∈ (𝐴 ∖ I ) ↔ (⟨𝑋, 𝑌⟩ ∈ 𝐴 ∧ 𝑋 ≠ 𝑌)))
Theorem	difres 30948	Case when class difference in unaffected by restriction. (Contributed by Thierry Arnoux, 1-Jan-2020.)
⊢ (𝐴 ⊆ (𝐵 × V) → (𝐴 ∖ (𝐶 ↾ 𝐵)) = (𝐴 ∖ 𝐶))
Theorem	imadifxp 30949	Image of the difference with a Cartesian product. (Contributed by Thierry Arnoux, 13-Dec-2017.)
⊢ (𝐶 ⊆ 𝐴 → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵))
Theorem	relfi 30950	A relation (set) is finite if and only if both its domain and range are finite. (Contributed by Thierry Arnoux, 27-Aug-2017.)
⊢ (Rel 𝐴 → (𝐴 ∈ Fin ↔ (dom 𝐴 ∈ Fin ∧ ran 𝐴 ∈ Fin)))
Theorem	reldisjun 30951	Split a relation into two disjoint parts based on its domain. (Contributed by Thierry Arnoux, 9-Oct-2023.)
⊢ ((Rel 𝑅 ∧ dom 𝑅 = (𝐴 ∪ 𝐵) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝑅 = ((𝑅 ↾ 𝐴) ∪ (𝑅 ↾ 𝐵)))
Theorem	0res 30952	Restriction of the empty function. (Contributed by Thierry Arnoux, 20-Nov-2023.)
⊢ (∅ ↾ 𝐴) = ∅
Theorem	funresdm1 30953	Restriction of a disjoint union to the domain of the first term. (Contributed by Thierry Arnoux, 9-Dec-2021.)
⊢ ((Rel 𝐴 ∧ (dom 𝐴 ∩ dom 𝐵) = ∅) → ((𝐴 ∪ 𝐵) ↾ dom 𝐴) = 𝐴)
Theorem	fnunres1 30954	Restriction of a disjoint union to the domain of the first function. (Contributed by Thierry Arnoux, 9-Dec-2021.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐹 ∪ 𝐺) ↾ 𝐴) = 𝐹)
Theorem	fcoinver 30955	Build an equivalence relation from a function. Two values are equivalent if they have the same image by the function. See also fcoinvbr 30956. (Contributed by Thierry Arnoux, 3-Jan-2020.)
⊢ (𝐹 Fn 𝑋 → (◡𝐹 ∘ 𝐹) Er 𝑋)
Theorem	fcoinvbr 30956	Binary relation for the equivalence relation from fcoinver 30955. (Contributed by Thierry Arnoux, 3-Jan-2020.)
⊢ ∼ = (◡𝐹 ∘ 𝐹)    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∼ 𝑌 ↔ (𝐹‘𝑋) = (𝐹‘𝑌)))
Theorem	brabgaf 30957*	The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.) (Revised by Thierry Arnoux, 17-May-2020.)
⊢ Ⅎ𝑥𝜓    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴𝑅𝐵 ↔ 𝜓))
Theorem	brelg 30958	Two things in a binary relation belong to the relation's domain. (Contributed by Thierry Arnoux, 29-Aug-2017.)
⊢ ((𝑅 ⊆ (𝐶 × 𝐷) ∧ 𝐴𝑅𝐵) → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
Theorem	br8d 30959*	Substitution for an eight-place predicate. (Contributed by Scott Fenton, 26-Sep-2013.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by Thierry Arnoux, 21-Mar-2019.)
⊢ (𝑎 = 𝐴 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑏 = 𝐵 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑐 = 𝐶 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑑 = 𝐷 → (𝜏 ↔ 𝜂))    &   ⊢ (𝑒 = 𝐸 → (𝜂 ↔ 𝜁))    &   ⊢ (𝑓 = 𝐹 → (𝜁 ↔ 𝜎))    &   ⊢ (𝑔 = 𝐺 → (𝜎 ↔ 𝜌))    &   ⊢ (ℎ = 𝐻 → (𝜌 ↔ 𝜇))    &   ⊢ (𝜑 → 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓)})    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩𝑅⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ 𝜇))
Theorem	opabdm 30960*	Domain of an ordered-pair class abstraction. (Contributed by Thierry Arnoux, 31-Aug-2017.)
⊢ (𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} → dom 𝑅 = {𝑥 ∣ ∃𝑦𝜑})
Theorem	opabrn 30961*	Range of an ordered-pair class abstraction. (Contributed by Thierry Arnoux, 31-Aug-2017.)
⊢ (𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} → ran 𝑅 = {𝑦 ∣ ∃𝑥𝜑})
Theorem	opabssi 30962*	Sufficient condition for a collection of ordered pairs to be a subclass of a relation. (Contributed by Peter Mazsa, 21-Oct-2019.) (Revised by Thierry Arnoux, 18-Feb-2022.)
⊢ (𝜑 → ⟨𝑥, 𝑦⟩ ∈ 𝐴)    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ 𝐴
Theorem	opabid2ss 30963*	One direction of opabid2 5740 which holds without a Rel 𝐴 requirement. (Contributed by Thierry Arnoux, 18-Feb-2022.)
⊢ {⟨𝑥, 𝑦⟩ ∣ ⟨𝑥, 𝑦⟩ ∈ 𝐴} ⊆ 𝐴
Theorem	ssrelf 30964*	A subclass relationship depends only on a relation's ordered pairs. Theorem 3.2(i) of [Monk1] p. 33. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Revised by Thierry Arnoux, 6-Nov-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
Theorem	eqrelrd2 30965*	A version of eqrelrdv2 5707 with explicit nonfree declarations. (Contributed by Thierry Arnoux, 28-Aug-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵))    ⇒   ⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → 𝐴 = 𝐵)
Theorem	erbr3b 30966	Biconditional for equivalent elements. (Contributed by Thierry Arnoux, 6-Jan-2020.)
⊢ ((𝑅 Er 𝑋 ∧ 𝐴𝑅𝐵) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
Theorem	iunsnima 30967	Image of a singleton by an indexed union involving that singleton. (Contributed by Thierry Arnoux, 10-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) “ {𝑥}) = 𝐵)
Theorem	iunsnima2 30968*	Version of iunsnima 30967 with different variables. (Contributed by Thierry Arnoux, 22-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝑌 ∈ 𝐴) → (∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) “ {𝑌}) = 𝐶)
20.3.4.2  Functions - misc additions
Theorem	ac6sf2 30969*	Alternate version of ac6 10245 with bound-variable hypothesis. (Contributed by NM, 2-Mar-2008.) (Revised by Thierry Arnoux, 17-May-2020.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓))
Theorem	fnresin 30970	Restriction of a function with a subclass of its domain. (Contributed by Thierry Arnoux, 10-Oct-2017.)
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐵) Fn (𝐴 ∩ 𝐵))
Theorem	f1o3d 30971*	Describe an implicit one-to-one onto function. (Contributed by Thierry Arnoux, 23-Apr-2017.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶))    ⇒   ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐵 ∧ ◡𝐹 = (𝑦 ∈ 𝐵 ↦ 𝐷)))
Theorem	eldmne0 30972	A function of nonempty domain is not empty. (Contributed by Thierry Arnoux, 20-Nov-2023.)
⊢ (𝑋 ∈ dom 𝐹 → 𝐹 ≠ ∅)
Theorem	f1rnen 30973	Equinumerosity of the range of an injective function. (Contributed by Thierry Arnoux, 7-Jul-2023.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉) → ran 𝐹 ≈ 𝐴)
Theorem	rinvf1o 30974	Sufficient conditions for the restriction of an involution to be a bijection. (Contributed by Thierry Arnoux, 7-Dec-2016.)
⊢ Fun 𝐹    &   ⊢ ◡𝐹 = 𝐹    &   ⊢ (𝐹 “ 𝐴) ⊆ 𝐵    &   ⊢ (𝐹 “ 𝐵) ⊆ 𝐴    &   ⊢ 𝐴 ⊆ dom 𝐹    &   ⊢ 𝐵 ⊆ dom 𝐹    ⇒   ⊢ (𝐹 ↾ 𝐴):𝐴–1-1-onto→𝐵
Theorem	fresf1o 30975	Conditions for a restriction to be a one-to-one onto function. (Contributed by Thierry Arnoux, 7-Dec-2016.)
⊢ ((Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹 ∧ Fun (◡𝐹 ↾ 𝐶)) → (𝐹 ↾ (◡𝐹 “ 𝐶)):(◡𝐹 “ 𝐶)–1-1-onto→𝐶)
Theorem	nfpconfp 30976	The set of fixed points of 𝐹 is the complement of the set of points moved by 𝐹. (Contributed by Thierry Arnoux, 17-Nov-2023.)
⊢ (𝐹 Fn 𝐴 → (𝐴 ∖ dom (𝐹 ∖ I )) = dom (𝐹 ∩ I ))
Theorem	fmptco1f1o 30977*	The action of composing (to the right) with a bijection is itself a bijection of functions. (Contributed by Thierry Arnoux, 3-Jan-2021.)
⊢ 𝐴 = (𝑅 ↑m 𝐸)    &   ⊢ 𝐵 = (𝑅 ↑m 𝐷)    &   ⊢ 𝐹 = (𝑓 ∈ 𝐴 ↦ (𝑓 ∘ 𝑇))    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑇:𝐷–1-1-onto→𝐸)    ⇒   ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵)
Theorem	cofmpt2 30978*	Express composition of a maps-to function with another function in a maps-to notation. (Contributed by Thierry Arnoux, 15-Jul-2023.)
⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑥)) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ 𝐸)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝐶) ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝐷))
Theorem	f1mptrn 30979*	Express injection for a mapping operation. (Contributed by Thierry Arnoux, 3-May-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ∃!𝑥 ∈ 𝐴 𝑦 = 𝐵)    ⇒   ⊢ (𝜑 → Fun ◡(𝑥 ∈ 𝐴 ↦ 𝐵))
Theorem	dfimafnf 30980*	Alternate definition of the image of a function. (Contributed by Raph Levien, 20-Nov-2006.) (Revised by Thierry Arnoux, 24-Apr-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐹    ⇒   ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 “ 𝐴) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
Theorem	funimass4f 30981	Membership relation for the values of a function whose image is a subclass. (Contributed by Thierry Arnoux, 24-Apr-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝐹    ⇒   ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → ((𝐹 “ 𝐴) ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
Theorem	elimampt 30982*	Membership in the image of a mapping. (Contributed by Thierry Arnoux, 3-Jan-2022.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝐶 ∈ (𝐹 “ 𝐷) ↔ ∃𝑥 ∈ 𝐷 𝐶 = 𝐵))
Theorem	suppss2f 30983*	Show that the support of a function is contained in a set. (Contributed by Thierry Arnoux, 22-Jun-2017.) (Revised by AV, 1-Sep-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ Ⅎ𝑘𝑊    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → 𝐵 = 𝑍)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 𝑍) ⊆ 𝑊)
Theorem	fovcld 30984	Closure law for an operation. (Contributed by NM, 19-Apr-2007.) (Revised by Thierry Arnoux, 17-Feb-2017.)
⊢ (𝜑 → 𝐹:(𝑅 × 𝑆)⟶𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)
Theorem	ofrn 30985	The range of the function operation. (Contributed by Thierry Arnoux, 8-Jan-2017.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐵)    &   ⊢ (𝜑 → + :(𝐵 × 𝐵)⟶𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ran (𝐹 ∘f + 𝐺) ⊆ 𝐶)
Theorem	ofrn2 30986	The range of the function operation. (Contributed by Thierry Arnoux, 21-Mar-2017.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐵)    &   ⊢ (𝜑 → + :(𝐵 × 𝐵)⟶𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ran (𝐹 ∘f + 𝐺) ⊆ ( + “ (ran 𝐹 × ran 𝐺)))
Theorem	off2 30987*	The function operation produces a function - alternative form with all antecedents as deduction. (Contributed by Thierry Arnoux, 17-Feb-2017.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝑇)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺):𝐶⟶𝑈)
Theorem	ofresid 30988	Applying an operation restricted to the range of the functions does not change the function operation. (Contributed by Thierry Arnoux, 14-Feb-2018.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝐹 ∘f (𝑅 ↾ (𝐵 × 𝐵))𝐺))
Theorem	fimarab 30989*	Expressing the image of a set as a restricted abstract builder. (Contributed by Thierry Arnoux, 27-Jan-2020.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑋 ⊆ 𝐴) → (𝐹 “ 𝑋) = {𝑦 ∈ 𝐵 ∣ ∃𝑥 ∈ 𝑋 (𝐹‘𝑥) = 𝑦})
Theorem	unipreima 30990*	Preimage of a class union. (Contributed by Thierry Arnoux, 7-Feb-2017.)
⊢ (Fun 𝐹 → (◡𝐹 “ ∪ 𝐴) = ∪ 𝑥 ∈ 𝐴 (◡𝐹 “ 𝑥))
Theorem	opfv 30991	Value of a function producing ordered pairs. (Contributed by Thierry Arnoux, 3-Jan-2017.)
⊢ (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) = ⟨((1st ∘ 𝐹)‘𝑥), ((2nd ∘ 𝐹)‘𝑥)⟩)
Theorem	xppreima 30992	The preimage of a Cartesian product is the intersection of the preimages of each component function. (Contributed by Thierry Arnoux, 6-Jun-2017.)
⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) → (◡𝐹 “ (𝑌 × 𝑍)) = ((◡(1st ∘ 𝐹) “ 𝑌) ∩ (◡(2nd ∘ 𝐹) “ 𝑍)))
Theorem	2ndimaxp 30993	Image of a cartesian product by 2nd. (Contributed by Thierry Arnoux, 23-Jun-2024.)
⊢ (𝐴 ≠ ∅ → (2nd “ (𝐴 × 𝐵)) = 𝐵)
Theorem	djussxp2 30994*	Stronger version of djussxp 5757. (Contributed by Thierry Arnoux, 23-Jun-2024.)
⊢ ∪ 𝑘 ∈ 𝐴 ({𝑘} × 𝐵) ⊆ (𝐴 × ∪ 𝑘 ∈ 𝐴 𝐵)
Theorem	2ndresdju 30995*	The 2nd function restricted to a disjoint union is injective. (Contributed by Thierry Arnoux, 23-Jun-2024.)
⊢ 𝑈 = ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝑋 𝐶)    &   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴)    ⇒   ⊢ (𝜑 → (2nd ↾ 𝑈):𝑈–1-1→𝐴)
Theorem	2ndresdjuf1o 30996*	The 2nd function restricted to a disjoint union is a bijection. See also e.g. 2ndconst 7950. (Contributed by Thierry Arnoux, 23-Jun-2024.)
⊢ 𝑈 = ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝑋 𝐶)    &   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴)    ⇒   ⊢ (𝜑 → (2nd ↾ 𝑈):𝑈–1-1-onto→𝐴)
Theorem	xppreima2 30997*	The preimage of a Cartesian product is the intersection of the preimages of each component function. (Contributed by Thierry Arnoux, 7-Jun-2017.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐶)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑥)⟩)    ⇒   ⊢ (𝜑 → (◡𝐻 “ (𝑌 × 𝑍)) = ((◡𝐹 “ 𝑌) ∩ (◡𝐺 “ 𝑍)))
Theorem	abfmpunirn 30998*	Membership in a union of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 28-Sep-2016.)
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∣ 𝜑})    &   ⊢ {𝑦 ∣ 𝜑} ∈ V    &   ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐵 ∈ ∪ ran 𝐹 ↔ (𝐵 ∈ V ∧ ∃𝑥 ∈ 𝑉 𝜓))
Theorem	rabfmpunirn 30999*	Membership in a union of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 30-Sep-2016.)
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ 𝑊 ∣ 𝜑})    &   ⊢ 𝑊 ∈ V    &   ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐵 ∈ ∪ ran 𝐹 ↔ ∃𝑥 ∈ 𝑉 (𝐵 ∈ 𝑊 ∧ 𝜓))
Theorem	abfmpeld 31000*	Membership in an element of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 19-Oct-2016.)
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∣ 𝜓})    &   ⊢ (𝜑 → {𝑦 ∣ 𝜓} ∈ V)    &   ⊢ (𝜑 → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∈ (𝐹‘𝐴) ↔ 𝜒)))