P. 331 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33001-33100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	19.9d2r 33001*	A deduction version of one direction of 19.9 2241 with two variables. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	r19.29ffa 33002*	A commonly used pattern based on r19.29 3125, version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.)
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) → 𝜒)
Theorem	reu6dv 33003*	A condition which implies existential uniqueness. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝑥 = 𝐵))    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝐴 𝜓)
21.3.2.3  Equality
Theorem	eqtrb 33004	A transposition of equality. (Contributed by Thierry Arnoux, 20-Aug-2023.)
⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) ↔ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶))
Theorem	eqelbid 33005*	A variable elimination law for equality within a given set 𝐴. See equvel 2485. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝑥 = 𝐵 ↔ 𝑥 = 𝐶) ↔ 𝐵 = 𝐶))
21.3.2.4  Double restricted existential uniqueness quantification
Theorem	opsbc2ie 33006*	Conversion of implicit substitution to explicit class substitution for ordered pairs. (Contributed by Thierry Arnoux, 4-Jul-2023.)
⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜑 ↔ 𝜒))    ⇒   ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ [𝑦 / 𝑏][𝑥 / 𝑎]𝜒))
Theorem	opreu2reuALT 33007*	Correspondence between uniqueness of ordered pairs and double restricted existential uniqueness quantification. Alternate proof of one direction only, use opreu2reurex 6286 instead. (Contributed by Thierry Arnoux, 4-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜑 ↔ 𝜒))    ⇒   ⊢ ((∃!𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ ∃!𝑏 ∈ 𝐵 ∃𝑎 ∈ 𝐴 𝜒) → ∃!𝑝 ∈ (𝐴 × 𝐵)𝜑)
21.3.2.5  Double restricted existential uniqueness quantification syntax
Syntax	w2reu 33008	Syntax for double restricted existential uniqueness quantification.
wff ∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑
Definition	df-2reu 33009	Define the double restricted existential uniqueness quantifier. (Contributed by Thierry Arnoux, 4-Jul-2023.)
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑))
Theorem	2reucom 33010	Double restricted existential uniqueness commutes. (Contributed by Thierry Arnoux, 4-Jul-2023.)
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 ↔ ∃!𝑦 ∈ 𝐵 , 𝑥 ∈ 𝐴𝜑)
Theorem	2reu2rex1 33011	Double restricted existential uniqueness implies double restricted existence. (Contributed by Thierry Arnoux, 4-Jul-2023.)
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
Theorem	2reureurex 33012	Double restricted existential uniqueness implies restricted existential uniqueness with restricted existence. (Contributed by AV, 5-Jul-2023.)
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 → ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
Theorem	2reu2reu2 33013*	Double restricted existential uniqueness implies two nested restricted existential uniqueness. (Contributed by AV, 5-Jul-2023.)
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 → ∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑)
Theorem	opreu2reu1 33014*	Equivalent definition of the double restricted existential uniqueness quantifier, using uniqueness of ordered pairs. (Contributed by Thierry Arnoux, 4-Jul-2023.)
⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝜒 ↔ 𝜑))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 ↔ ∃!𝑝 ∈ (𝐴 × 𝐵)𝜒)
Theorem	sq2reunnltb 33015*	There exists a unique decomposition of a prime as a sum of squares of two different positive integers iff the prime is of the form 4𝑘 + 1. Double restricted existential uniqueness variant of 2sqreunnltb 27752. (Contributed by AV, 5-Jul-2023.)
⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ ∃!𝑎 ∈ ℕ , 𝑏 ∈ ℕ(𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)))
Theorem	addsqnot2reu 33016*	For each complex number 𝐶, there does not uniquely exist two complex numbers 𝑎 and 𝑏, with 𝑏 squared and added to 𝑎 resulting in the given complex number 𝐶. Double restricted existential uniqueness variant of addsqn2reurex2 27736. (Contributed by AV, 5-Jul-2023.)
⊢ (𝐶 ∈ ℂ → ¬ ∃!𝑎 ∈ ℂ , 𝑏 ∈ ℂ(𝑎 + (𝑏↑2)) = 𝐶)
21.3.2.6  Substitution (without distinct variables) - misc additions
Theorem	sbceqbidf 33017	Equality theorem for class substitution. (Contributed by Thierry Arnoux, 4-Sep-2018.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜒))
Theorem	sbcies 33018*	A special version of class substitution commonly used for structures. (Contributed by Thierry Arnoux, 14-Mar-2019.)
⊢ 𝐴 = (𝐸‘𝑊)    &   ⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝑤 = 𝑊 → ([(𝐸‘𝑤) / 𝑎]𝜓 ↔ 𝜑))
21.3.2.7  Existential "at most one" - misc additions
Theorem	mo5f 33019*	Alternate definition of "at most one." (Contributed by Thierry Arnoux, 1-Mar-2017.)
⊢ Ⅎ𝑖𝜑    &   ⊢ Ⅎ𝑗𝜑    ⇒   ⊢ (∃*𝑥𝜑 ↔ ∀𝑖∀𝑗(([𝑖 / 𝑥]𝜑 ∧ [𝑗 / 𝑥]𝜑) → 𝑖 = 𝑗))
Theorem	nmo 33020*	Negation of "at most one". (Contributed by Thierry Arnoux, 26-Feb-2017.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (¬ ∃*𝑥𝜑 ↔ ∀𝑦∃𝑥(𝜑 ∧ 𝑥 ≠ 𝑦))
21.3.2.8  Existential uniqueness - misc additions
Theorem	reuxfrdf 33021*	Transfer existential uniqueness from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. Cf. reuxfrd 3705 (Contributed by Thierry Arnoux, 7-Apr-2017.) (Revised by Thierry Arnoux, 8-Oct-2017.) (Revised by Thierry Arnoux, 30-Mar-2018.)
⊢ Ⅎ𝑦𝐵    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃*𝑦 ∈ 𝐶 𝑥 = 𝐴)    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦 ∈ 𝐶 𝜓))
Theorem	rexunirn 33022*	Restricted existential quantification over the union of the range of a function. Cf. rexrn 7075 and eluni2 4870. (Contributed by Thierry Arnoux, 19-Sep-2017.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝑥 ∈ 𝐴 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑦 ∈ ∪ ran 𝐹𝜑)
21.3.2.9  Restricted "at most one" - misc additions
Theorem	rmoxfrd 33023*	Transfer "at most one" restricted quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by Thierry Arnoux, 7-Apr-2017.) (Revised by Thierry Arnoux, 8-Oct-2017.)
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃!𝑦 ∈ 𝐶 𝑥 = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐵 𝜓 ↔ ∃*𝑦 ∈ 𝐶 𝜒))
Theorem	rmoun 33024	"At most one" restricted existential quantifier for a union implies the same quantifier on both sets. (Contributed by Thierry Arnoux, 27-Nov-2023.)
⊢ (∃*𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 → (∃*𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐵 𝜑))
Theorem	rmounid 33025*	A case where an "at most one" restricted existential quantifier for a union is equivalent to such a quantifier for one of the sets. (Contributed by Thierry Arnoux, 27-Nov-2023.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ¬ 𝜓)    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ (𝐴 ∪ 𝐵)𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜓))
21.3.2.10  Restricted iota (description binder)
Theorem	riotaeqbidva 33026*	Equivalent wff's yield equal restricted definition binders (deduction form). (raleqbidva 3325 analog.) (Contributed by Thierry Arnoux, 29-Jan-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐵 𝜒))
21.3.3  General Set Theory
21.3.3.1  Class abstractions (a.k.a. class builders)
Theorem	dmrab 33027*	Domain of a restricted class abstraction over a cartesian product. (Contributed by Thierry Arnoux, 3-Jul-2023.)
⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ dom {𝑧 ∈ (𝐴 × 𝐵) ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ 𝐵 𝜓}
Theorem	difrab2 33028	Difference of two restricted class abstractions. Compare with difrab 4263. (Contributed by Thierry Arnoux, 3-Jan-2022.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∖ {𝑥 ∈ 𝐵 ∣ 𝜑}) = {𝑥 ∈ (𝐴 ∖ 𝐵) ∣ 𝜑}
Theorem	rabexgfGS 33029	Separation Scheme in terms of a restricted class abstraction. To be removed in profit of Glauco's equivalent version. (Contributed by Thierry Arnoux, 11-May-2017.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
Theorem	rabsnel 33030*	Truth implied by equality of a restricted class abstraction and a singleton. (Contributed by Thierry Arnoux, 15-Sep-2018.)
⊢ 𝐵 ∈ V    ⇒   ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = {𝐵} → 𝐵 ∈ 𝐴)
Theorem	rabsspr 33031*	Conditions for a restricted class abstraction to be a subset of an unordered pair. (Contributed by Thierry Arnoux, 6-Jul-2025.)
⊢ ({𝑥 ∈ 𝑉 ∣ 𝜑} ⊆ {𝑋, 𝑌} ↔ ∀𝑥 ∈ 𝑉 (𝜑 → (𝑥 = 𝑋 ∨ 𝑥 = 𝑌)))
Theorem	rabsstp 33032*	Conditions for a restricted class abstraction to be a subset of an unordered triple. (Contributed by Thierry Arnoux, 6-Jul-2025.)
⊢ ({𝑥 ∈ 𝑉 ∣ 𝜑} ⊆ {𝑋, 𝑌, 𝑍} ↔ ∀𝑥 ∈ 𝑉 (𝜑 → (𝑥 = 𝑋 ∨ 𝑥 = 𝑌 ∨ 𝑥 = 𝑍)))
Theorem	3unrab 33033	Union of three restricted class abstractions. (Contributed by Thierry Arnoux, 6-Jul-2025.)
⊢ (({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) ∪ {𝑥 ∈ 𝐴 ∣ 𝜒}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓 ∨ 𝜒)}
Theorem	foresf1o 33034*	From a surjective function, *choose* a subset of the domain, such that the restricted function is bijective. (Contributed by Thierry Arnoux, 27-Jan-2020.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) → ∃𝑥 ∈ 𝒫 𝐴(𝐹 ↾ 𝑥):𝑥–1-1-onto→𝐵)
Theorem	rabfodom 33035*	Domination relation for restricted abstract class builders, based on a surjective function. (Contributed by Thierry Arnoux, 27-Jan-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥)) → (𝜒 ↔ 𝜓))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴–onto→𝐵)    ⇒   ⊢ (𝜑 → {𝑦 ∈ 𝐵 ∣ 𝜒} ≼ {𝑥 ∈ 𝐴 ∣ 𝜓})
Theorem	rabrexfi 33036*	Conditions for a class abstraction with a restricted existential quantification to be finite. (Contributed by Thierry Arnoux, 6-Jul-2025.)
⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → {𝑥 ∈ 𝐴 ∣ 𝜓} ∈ Fin)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ 𝐵 𝜓} ∈ Fin)
21.3.3.2  Image Sets
Theorem	abrexdomjm 33037*	An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑦 ∈ 𝐴 → ∃*𝑥𝜑)    ⇒   ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝜑} ≼ 𝐴)
Theorem	abrexdom2jm 33038*	An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 = 𝐵} ≼ 𝐴)
Theorem	abrexexd 33039*	Existence of a class abstraction of existentially restricted sets. (Contributed by Thierry Arnoux, 10-May-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ (𝜑 → 𝐴 ∈ V)    ⇒   ⊢ (𝜑 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V)
Theorem	elabreximd 33040*	Class substitution in an image set. (Contributed by Thierry Arnoux, 30-Dec-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (𝐴 = 𝐵 → (𝜒 ↔ 𝜓))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐶 𝑦 = 𝐵}) → 𝜒)
Theorem	elabreximdv 33041*	Class substitution in an image set. (Contributed by Thierry Arnoux, 30-Dec-2016.)
⊢ (𝐴 = 𝐵 → (𝜒 ↔ 𝜓))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐶 𝑦 = 𝐵}) → 𝜒)
Theorem	abrexss 33042*	A necessary condition for an image set to be a subset. (Contributed by Thierry Arnoux, 6-Feb-2017.)
⊢ Ⅎ𝑥𝐶    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ⊆ 𝐶)
21.3.3.3  Set relations and operations - misc additions
Theorem	nelun 33043	Negated membership for a union. (Contributed by Thierry Arnoux, 13-Dec-2023.)
⊢ (𝐴 = (𝐵 ∪ 𝐶) → (¬ 𝑋 ∈ 𝐴 ↔ (¬ 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ 𝐶)))
Theorem	snsssng 33044	If a singleton is a subset of another, their members are equal. (Contributed by NM, 28-May-2006.) (Revised by Thierry Arnoux, 11-Apr-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ {𝐴} ⊆ {𝐵}) → 𝐴 = 𝐵)
Theorem	n0nsnel 33045*	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.) (Revised by Thierry Arnoux, 28-May-2025.)
⊢ ((𝐶 ∈ 𝐵 ∧ 𝐵 ≠ {𝐴}) → ∃𝑥 ∈ 𝐵 𝑥 ≠ 𝐴)
Theorem	inin 33046	Intersection with an intersection. (Contributed by Thierry Arnoux, 27-Dec-2016.)
⊢ (𝐴 ∩ (𝐴 ∩ 𝐵)) = (𝐴 ∩ 𝐵)
Theorem	difininv 33047	Condition for the intersections of two sets with a given set to be equal. (Contributed by Thierry Arnoux, 28-Dec-2021.)
⊢ ((((𝐴 ∖ 𝐶) ∩ 𝐵) = ∅ ∧ ((𝐶 ∖ 𝐴) ∩ 𝐵) = ∅) → (𝐴 ∩ 𝐵) = (𝐶 ∩ 𝐵))
Theorem	difeq 33048	Rewriting an equation with class difference, without using quantifiers. (Contributed by Thierry Arnoux, 24-Sep-2017.)
⊢ ((𝐴 ∖ 𝐵) = 𝐶 ↔ ((𝐶 ∩ 𝐵) = ∅ ∧ (𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵)))
Theorem	eqdif 33049	If both set differences of two sets are empty, those sets are equal. (Contributed by Thierry Arnoux, 16-Nov-2023.)
⊢ (((𝐴 ∖ 𝐵) = ∅ ∧ (𝐵 ∖ 𝐴) = ∅) → 𝐴 = 𝐵)
Theorem	indifbi 33050	Two ways to express equality relative to a class 𝐴. (Contributed by Thierry Arnoux, 23-Jun-2024.)
⊢ ((𝐴 ∩ 𝐵) = (𝐴 ∩ 𝐶) ↔ (𝐴 ∖ 𝐵) = (𝐴 ∖ 𝐶))
Theorem	diffib 33051	Case where diffi 9168 is a biconditional. (Contributed by Thierry Arnoux, 27-Jun-2024.)
⊢ (𝐵 ∈ Fin → (𝐴 ∈ Fin ↔ (𝐴 ∖ 𝐵) ∈ Fin))
Theorem	difxp1ss 33052	Difference law for Cartesian products. (Contributed by Thierry Arnoux, 24-Jul-2023.)
⊢ ((𝐴 ∖ 𝐶) × 𝐵) ⊆ (𝐴 × 𝐵)
Theorem	difxp2ss 33053	Difference law for Cartesian products. (Contributed by Thierry Arnoux, 24-Jul-2023.)
⊢ (𝐴 × (𝐵 ∖ 𝐶)) ⊆ (𝐴 × 𝐵)
Theorem	indifundif 33054	A remarkable equation with sets. (Contributed by Thierry Arnoux, 18-May-2020.)
⊢ (((𝐴 ∩ 𝐵) ∖ 𝐶) ∪ (𝐴 ∖ 𝐵)) = (𝐴 ∖ (𝐵 ∩ 𝐶))
Theorem	elpwincl1 33055	Closure of intersection with regard to elementhood to a power set. (Contributed by Thierry Arnoux, 18-May-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐵) ∈ 𝒫 𝐶)
Theorem	elpwdifcl 33056	Closure of class difference with regard to elementhood to a power set. (Contributed by Thierry Arnoux, 18-May-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐵) ∈ 𝒫 𝐶)
Theorem	elpwiuncl 33057*	Closure of indexed union with regard to elementhood to a power set. (Contributed by Thierry Arnoux, 27-May-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝒫 𝐶)    ⇒   ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝒫 𝐶)
21.3.3.4  Unordered pairs
Theorem	elpreq 33058	Equality wihin a pair. (Contributed by Thierry Arnoux, 23-Aug-2017.)
⊢ (𝜑 → 𝑋 ∈ {𝐴, 𝐵})    &   ⊢ (𝜑 → 𝑌 ∈ {𝐴, 𝐵})    &   ⊢ (𝜑 → (𝑋 = 𝐴 ↔ 𝑌 = 𝐴))    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	prssad 33059	If a pair is a subset of a class, the first element of the pair is an element of that class. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → {𝐴, 𝐵} ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	prssbd 33060	If a pair is a subset of a class, the second element of the pair is an element of that class. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → {𝐴, 𝐵} ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝐶)
Theorem	nelpr 33061	A set 𝐴 not in a pair is neither element of the pair. (Contributed by Thierry Arnoux, 20-Nov-2023.)
⊢ (𝐴 ∈ 𝑉 → (¬ 𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶)))
Theorem	inpr0 33062	Rewrite an empty intersection with a pair. (Contributed by Thierry Arnoux, 20-Nov-2023.)
⊢ ((𝐴 ∩ {𝐵, 𝐶}) = ∅ ↔ (¬ 𝐵 ∈ 𝐴 ∧ ¬ 𝐶 ∈ 𝐴))
Theorem	neldifpr1 33063	The first element of a pair is not an element of a difference with this pair. (Contributed by Thierry Arnoux, 20-Nov-2023.)
⊢ ¬ 𝐴 ∈ (𝐶 ∖ {𝐴, 𝐵})
Theorem	neldifpr2 33064	The second element of a pair is not an element of a difference with this pair. (Contributed by Thierry Arnoux, 20-Nov-2023.)
⊢ ¬ 𝐵 ∈ (𝐶 ∖ {𝐴, 𝐵})
Theorem	unidifsnel 33065	The other element of a pair is an element of the pair. (Contributed by Thierry Arnoux, 26-Aug-2017.)
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) → ∪ (𝑃 ∖ {𝑋}) ∈ 𝑃)
Theorem	unidifsnne 33066	The other element of a pair is not the known element. (Contributed by Thierry Arnoux, 26-Aug-2017.)
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) → ∪ (𝑃 ∖ {𝑋}) ≠ 𝑋)
21.3.3.5  Unordered triples
Theorem	tpssg 33067	An unordered triple of elements of a class is a subset of the class. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) ↔ {𝐴, 𝐵, 𝐶} ⊆ 𝐷))
Theorem	tpssd 33068	Deduction version of tpssi : An unordered triple of elements of a class is a subset of that class. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐷)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵, 𝐶} ⊆ 𝐷)
Theorem	tpssad 33069	If an ordered triple is a subset of a class, the first element of the triple is an element of that class. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → {𝐴, 𝐵, 𝐶} ⊆ 𝐷)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐷)
Theorem	tpssbd 33070	If an ordered triple is a subset of a class, the second element of the triple is an element of that class. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → {𝐴, 𝐵, 𝐶} ⊆ 𝐷)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝐷)
Theorem	tpsscd 33071	If an ordered triple is a subset of a class, the third element of the triple is an element of that class. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → {𝐴, 𝐵, 𝐶} ⊆ 𝐷)    ⇒   ⊢ (𝜑 → 𝐶 ∈ 𝐷)
21.3.3.6  Conditional operator - misc additions
Theorem	ifeqeqx 33072*	An equality theorem tailored for ballotlemsf1o 35081. (Contributed by Thierry Arnoux, 14-Apr-2017.)
⊢ (𝑥 = 𝑋 → 𝐴 = 𝐶)    &   ⊢ (𝑥 = 𝑌 → 𝐵 = 𝑎)    &   ⊢ (𝑥 = 𝑋 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑥 = 𝑌 → (𝜒 ↔ 𝜓))    &   ⊢ (𝜑 → 𝑎 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    ⇒   ⊢ ((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) → 𝑎 = if(𝜒, 𝐴, 𝐵))
Theorem	elimifd 33073	Elimination of a conditional operator contained in a wff 𝜒. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (𝜑 → (if(𝜓, 𝐴, 𝐵) = 𝐴 → (𝜒 ↔ 𝜃)))    &   ⊢ (𝜑 → (if(𝜓, 𝐴, 𝐵) = 𝐵 → (𝜒 ↔ 𝜏)))    ⇒   ⊢ (𝜑 → (𝜒 ↔ ((𝜓 ∧ 𝜃) ∨ (¬ 𝜓 ∧ 𝜏))))
Theorem	elim2if 33074	Elimination of two conditional operators contained in a wff 𝜒. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐴 → (𝜒 ↔ 𝜃))    &   ⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐵 → (𝜒 ↔ 𝜏))    &   ⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐶 → (𝜒 ↔ 𝜂))    ⇒   ⊢ (𝜒 ↔ ((𝜑 ∧ 𝜃) ∨ (¬ 𝜑 ∧ ((𝜓 ∧ 𝜏) ∨ (¬ 𝜓 ∧ 𝜂)))))
Theorem	elim2ifim 33075	Elimination of two conditional operators for an implication. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐴 → (𝜒 ↔ 𝜃))    &   ⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐵 → (𝜒 ↔ 𝜏))    &   ⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐶 → (𝜒 ↔ 𝜂))    &   ⊢ (𝜑 → 𝜃)    &   ⊢ ((¬ 𝜑 ∧ 𝜓) → 𝜏)    &   ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜂)    ⇒   ⊢ 𝜒
Theorem	ifeq3da 33076	Given an expression 𝐶 containing if(𝜓, 𝐸, 𝐹), substitute (hypotheses .1 and .2) and evaluate (hypotheses .3 and .4) it for both cases at the same time. (Contributed by Thierry Arnoux, 13-Dec-2021.)
⊢ (if(𝜓, 𝐸, 𝐹) = 𝐸 → 𝐶 = 𝐺)    &   ⊢ (if(𝜓, 𝐸, 𝐹) = 𝐹 → 𝐶 = 𝐻)    &   ⊢ (𝜑 → 𝐺 = 𝐴)    &   ⊢ (𝜑 → 𝐻 = 𝐵)    ⇒   ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = 𝐶)
Theorem	ifnetrue 33077	Deduce truth from a conditional operator value. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ ((𝐴 ≠ 𝐵 ∧ if(𝜑, 𝐴, 𝐵) = 𝐴) → 𝜑)
Theorem	ifnefals 33078	Deduce falsehood from a conditional operator value. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ ((𝐴 ≠ 𝐵 ∧ if(𝜑, 𝐴, 𝐵) = 𝐵) → ¬ 𝜑)
Theorem	ifnebib 33079	The converse of ifbi 4504 holds if the two values are not equal. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ (𝐴 ≠ 𝐵 → (if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐴, 𝐵) ↔ (𝜑 ↔ 𝜓)))
Theorem	ififcom 33080	Commute two nested conditionals. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = if(𝜓, if(𝜑, 𝐴, 𝐵), 𝐵)
21.3.3.7  Set union
Theorem	uniinn0 33081*	Sufficient and necessary condition for a union to intersect with a given set. (Contributed by Thierry Arnoux, 27-Jan-2020.)
⊢ ((∪ 𝐴 ∩ 𝐵) ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐵) ≠ ∅)
Theorem	difuncomp 33082	Express a class difference using unions and class complements. (Contributed by Thierry Arnoux, 21-Jun-2020.)
⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∖ 𝐵) = (𝐶 ∖ ((𝐶 ∖ 𝐴) ∪ 𝐵)))
Theorem	elpwunicl 33083	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.)
⊢ (𝜑 → 𝐴 ∈ 𝒫 𝒫 𝐵)    ⇒   ⊢ (𝜑 → ∪ 𝐴 ∈ 𝒫 𝐵)
21.3.3.8  Indexed union - misc additions
Theorem	cbviunf 33084*	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 33085	Equality deduction for indexed union, deduction version. (Contributed by Thierry Arnoux, 13-Mar-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷)
Theorem	iunin1f 33086	Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 5016 to recover Enderton's theorem. (Contributed by NM, 26-Mar-2004.) (Revised by Thierry Arnoux, 2-May-2020.)
⊢ Ⅎ𝑥𝐶    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶)
Theorem	ssiun3 33087*	Subset equivalence for an indexed union. (Contributed by Thierry Arnoux, 17-Oct-2016.)
⊢ (∀𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ↔ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	ssiun2sf 33088	Subset relationship for an indexed union. (Contributed by Thierry Arnoux, 31-Dec-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)    ⇒   ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	iuninc 33089*	The union of an increasing collection of sets is its last element. (Contributed by Thierry Arnoux, 22-Jan-2017.)
⊢ (𝜑 → 𝐹 Fn ℕ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)))    ⇒   ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ∪ 𝑛 ∈ (1...𝑖)(𝐹‘𝑛) = (𝐹‘𝑖))
Theorem	iundifdifd 33090*	The intersection of a set is the complement of the union of the complements. (Contributed by Thierry Arnoux, 19-Dec-2016.)
⊢ (𝐴 ⊆ 𝒫 𝑂 → (𝐴 ≠ ∅ → ∩ 𝐴 = (𝑂 ∖ ∪ 𝑥 ∈ 𝐴 (𝑂 ∖ 𝑥))))
Theorem	iundifdif 33091*	The intersection of a set is the complement of the union of the complements. TODO: shorten using iundifdifd 33090. (Contributed by Thierry Arnoux, 4-Sep-2016.)
⊢ 𝑂 ∈ V    &   ⊢ 𝐴 ⊆ 𝒫 𝑂    ⇒   ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 = (𝑂 ∖ ∪ 𝑥 ∈ 𝐴 (𝑂 ∖ 𝑥)))
Theorem	iunrdx 33092*	Re-index an indexed union. (Contributed by Thierry Arnoux, 6-Apr-2017.)
⊢ (𝜑 → 𝐹:𝐴–onto→𝐶)    &   ⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑥)) → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐶 𝐷)
Theorem	iunrnmptss 33093*	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 33094*	Appending a set to an indexed union. (Contributed by Thierry Arnoux, 20-Nov-2023.)
⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑋 ∈ 𝑉 → ∪ 𝑥 ∈ (𝐴 ∪ {𝑋})𝐵 = (∪ 𝑥 ∈ 𝐴 𝐵 ∪ 𝐶))
Theorem	iunxunpr 33095*	Appending two sets to an indexed union. (Contributed by Thierry Arnoux, 20-Nov-2023.)
⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶)    &   ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷)    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ∪ 𝑥 ∈ (𝐴 ∪ {𝑋, 𝑌})𝐵 = (∪ 𝑥 ∈ 𝐴 𝐵 ∪ (𝐶 ∪ 𝐷)))
Theorem	iunxpssiun1 33096*	Provide an upper bound for the indexed union of cartesian products. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ⊆ 𝐸)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 (𝐵 × 𝐶) ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 × 𝐸))
21.3.3.9  Indexed intersection - misc additions
Theorem	iinabrex 33097*	Rewriting an indexed intersection into an intersection of its image set. (Contributed by Thierry Arnoux, 15-Jun-2024.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})
21.3.3.10  Disjointness - misc additions
Theorem	disjnf 33098*	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 33099*	Change bound variables in a disjoint collection. (Contributed by Thierry Arnoux, 6-Apr-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶)
Theorem	disjss1f 33100	A subset of a disjoint collection is disjoint. (Contributed by Thierry Arnoux, 6-Apr-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ⊆ 𝐵 → (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐴 𝐶))