P. 52 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 5101-5200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	disjiund 5101*	Conditions for a collection of index unions of sets 𝐴(𝑎, 𝑏) for 𝑎 ∈ 𝑉 and 𝑏 ∈ 𝑊 to be disjoint. (Contributed by AV, 9-Jan-2022.)
⊢ (𝑎 = 𝑐 → 𝐴 = 𝐶)    &   ⊢ (𝑏 = 𝑑 → 𝐶 = 𝐷)    &   ⊢ (𝑎 = 𝑐 → 𝑊 = 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐷) → 𝑎 = 𝑐)    ⇒   ⊢ (𝜑 → Disj 𝑎 ∈ 𝑉 ∪ 𝑏 ∈ 𝑊 𝐴)
Theorem	sndisj 5102	Any collection of singletons is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Disj 𝑥 ∈ 𝐴 {𝑥}
Theorem	0disj 5103	Any collection of empty sets is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Disj 𝑥 ∈ 𝐴 ∅
Theorem	disjxsn 5104*	A singleton collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Disj 𝑥 ∈ {𝐴}𝐵
Theorem	disjx0 5105	An empty collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Disj 𝑥 ∈ ∅ 𝐵
Theorem	disjprg 5106*	A pair collection is disjoint iff the two sets in the family have empty intersection. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) → (Disj 𝑥 ∈ {𝐴, 𝐵}𝐶 ↔ (𝐷 ∩ 𝐸) = ∅))
Theorem	disjxiun 5107*	An indexed union of a disjoint collection of disjoint collections is disjoint if each component is disjoint, and the disjoint unions in the collection are also disjoint. Note that 𝐵(𝑦) and 𝐶(𝑥) may have the displayed free variables. (Contributed by Mario Carneiro, 14-Nov-2016.) (Proof shortened by JJ, 27-May-2021.)
⊢ (Disj 𝑦 ∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 ↔ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶)))
Theorem	disjxun 5108*	The union of two disjoint collections. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝐴 ∩ 𝐵) = ∅ → (Disj 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 ↔ (Disj 𝑥 ∈ 𝐴 𝐶 ∧ Disj 𝑥 ∈ 𝐵 𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝐶 ∩ 𝐷) = ∅)))
Theorem	disjss3 5109*	Expand a disjoint collection with any number of empty sets. (Contributed by Mario Carneiro, 15-Nov-2016.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐴)𝐶 = ∅) → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶))
2.1.23  Binary relations
Syntax	wbr 5110	Extend wff notation to include the general binary relation predicate. Note that the syntax is simply three class symbols in a row. Since binary relations are the only possible wff expressions consisting of three class expressions in a row, the syntax is unambiguous. (For an example of how syntax could become ambiguous if we are not careful, see the comment in cneg 11443.)
wff 𝐴𝑅𝐵
Definition	df-br 5111	Define a general binary relation. Note that the syntax is simply three class symbols in a row. Definition 6.18 of [TakeutiZaring] p. 29 generalized to arbitrary classes. Class 𝑅 often denotes a relation such as "< " that compares two classes 𝐴 and 𝐵, which might be numbers such as 1 and 2 (see df-ltxr 11249 for the specific definition of <). As a wff, relations are true or false. For example, (𝑅 = {⟨2, 6⟩, ⟨3, 9⟩} → 3𝑅9) (ex-br 30763). Often class 𝑅 meets the Rel criteria to be defined in df-rel 5670, and in particular 𝑅 may be a function (see df-fun 6540). This definition of relations is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e., are not sets). On the other hand, we often find uses for this definition when 𝑅 is a proper class (see for example iprc 7909). (Contributed by NM, 31-Dec-1993.)
⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
Theorem	breq 5112	Equality theorem for binary relations. (Contributed by NM, 4-Jun-1995.)
⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵))
Theorem	breq1 5113	Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
Theorem	breq2 5114	Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))
Theorem	breq12 5115	Equality theorem for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
Theorem	breqi 5116	Equality inference for binary relations. (Contributed by NM, 19-Feb-2005.)
⊢ 𝑅 = 𝑆    ⇒   ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)
Theorem	breq1i 5117	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)
Theorem	breq2i 5118	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵)
Theorem	breq12i 5119	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)
Theorem	breq1d 5120	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
Theorem	breqd 5121	Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷))
Theorem	breq2d 5122	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))
Theorem	breq12d 5123	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
Theorem	breq123d 5124	Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝑅 = 𝑆)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑆𝐷))
Theorem	breqdi 5125	Equality deduction for a binary relation. (Contributed by Thierry Arnoux, 5-Oct-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶𝐴𝐷)    ⇒   ⊢ (𝜑 → 𝐶𝐵𝐷)
Theorem	breqan12d 5126	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
Theorem	breqan12rd 5127	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
Theorem	breq1dd 5128	Equality deduction for a binary relation. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐵𝑅𝐶)
Theorem	breq2dd 5129	Equality deduction for a binary relation. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶𝑅𝐴)    ⇒   ⊢ (𝜑 → 𝐶𝑅𝐵)
Theorem	eqnbrtrd 5130	Substitution of equal classes into the negation of a binary relation. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → ¬ 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → ¬ 𝐴𝑅𝐶)
Theorem	nbrne1 5131	Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.)
⊢ ((𝐴𝑅𝐵 ∧ ¬ 𝐴𝑅𝐶) → 𝐵 ≠ 𝐶)
Theorem	nbrne2 5132	Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.)
⊢ ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴 ≠ 𝐵)
Theorem	eqbrtri 5133	Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵𝑅𝐶    ⇒   ⊢ 𝐴𝑅𝐶
Theorem	eqbrtrd 5134	Substitution of equal classes into a binary relation. (Contributed by NM, 8-Oct-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	eqbrtrri 5135	Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐴𝑅𝐶    ⇒   ⊢ 𝐵𝑅𝐶
Theorem	eqbrtrrd 5136	Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐵𝑅𝐶)
Theorem	breqtri 5137	Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)
⊢ 𝐴𝑅𝐵    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ 𝐴𝑅𝐶
Theorem	breqtrd 5138	Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	breqtrri 5139	Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)
⊢ 𝐴𝑅𝐵    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ 𝐴𝑅𝐶
Theorem	breqtrrd 5140	Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	3brtr3i 5141	Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.)
⊢ 𝐴𝑅𝐵    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ 𝐶𝑅𝐷
Theorem	3brtr4i 5142	Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.)
⊢ 𝐴𝑅𝐵    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ 𝐶𝑅𝐷
Theorem	3brtr3d 5143	Substitution of equality into both sides of a binary relation. (Contributed by NM, 18-Oct-1999.)
⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐶𝑅𝐷)
Theorem	3brtr4d 5144	Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.)
⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐴)    &   ⊢ (𝜑 → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐶𝑅𝐷)
Theorem	3brtr3g 5145	Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.)
⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ (𝜑 → 𝐶𝑅𝐷)
Theorem	3brtr4g 5146	Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.)
⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ (𝜑 → 𝐶𝑅𝐷)
Theorem	eqbrtrid 5147	A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	eqbrtrrid 5148	A chained equality inference for a binary relation. (Contributed by NM, 17-Sep-2004.)
⊢ 𝐵 = 𝐴    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	breqtrid 5149	A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
⊢ 𝐴𝑅𝐵    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	breqtrrid 5150	A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
⊢ 𝐴𝑅𝐵    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	eqbrtrdi 5151	A chained equality inference for a binary relation. (Contributed by NM, 12-Oct-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐵𝑅𝐶    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	eqbrtrrdi 5152	A chained equality inference for a binary relation. (Contributed by NM, 4-Jan-2006.)
⊢ (𝜑 → 𝐵 = 𝐴)    &   ⊢ 𝐵𝑅𝐶    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	breqtrdi 5153	A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	breqtrrdi 5154	A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	ssbrd 5155	Deduction from a subclass relationship of binary relations. (Contributed by NM, 30-Apr-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷))
Theorem	ssbr 5156	Implication from a subclass relationship of binary relations. (Contributed by Peter Mazsa, 11-Nov-2019.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷))
Theorem	ssbri 5157	Inference from a subclass relationship of binary relations. (Contributed by NM, 28-Mar-2007.) (Revised by Mario Carneiro, 8-Feb-2015.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ (𝐶𝐴𝐷 → 𝐶𝐵𝐷)
Theorem	nfbrd 5158	Deduction version of bound-variable hypothesis builder nfbr 5159. (Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝑅)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 𝐴𝑅𝐵)
Theorem	nfbr 5159	Bound-variable hypothesis builder for binary relation. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴𝑅𝐵
Theorem	brab1 5160*	Relationship between a binary relation and a class abstraction. (Contributed by Andrew Salmon, 8-Jul-2011.)
⊢ (𝑥𝑅𝐴 ↔ 𝑥 ∈ {𝑧 ∣ 𝑧𝑅𝐴})
Theorem	br0 5161	The empty binary relation never holds. (Contributed by NM, 23-Aug-2018.)
⊢ ¬ 𝐴∅𝐵
Theorem	brne0 5162	If two sets are in a binary relation, the relation cannot be empty. (Contributed by Alexander van der Vekens, 7-Jul-2018.)
⊢ (𝐴𝑅𝐵 → 𝑅 ≠ ∅)
Theorem	brun 5163	The union of two binary relations. (Contributed by NM, 21-Dec-2008.)
⊢ (𝐴(𝑅 ∪ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∨ 𝐴𝑆𝐵))
Theorem	brin 5164	The intersection of two relations. (Contributed by FL, 7-Oct-2008.)
⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵))
Theorem	brdif 5165	The difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2011.)
⊢ (𝐴(𝑅 ∖ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵))
Theorem	sbcbr123 5166	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) (Revised by NM, 22-Aug-2018.)
⊢ ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵⦋𝐴 / 𝑥⦌𝑅⦋𝐴 / 𝑥⦌𝐶)
Theorem	sbcbr 5167*	Move substitution in and out of a binary relation. (Contributed by NM, 23-Aug-2018.)
⊢ ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ 𝐵⦋𝐴 / 𝑥⦌𝑅𝐶)
Theorem	sbcbr12g 5168*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵𝑅⦋𝐴 / 𝑥⦌𝐶))
Theorem	sbcbr1g 5169*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵𝑅𝐶))
Theorem	sbcbr2g 5170*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ 𝐵𝑅⦋𝐴 / 𝑥⦌𝐶))
Theorem	brsymdif 5171	Characterization of the symmetric difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ (𝐴(𝑅 △ 𝑆)𝐵 ↔ ¬ (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵))
Theorem	brralrspcev 5172*	Restricted existential specialization with a restricted universal quantifier over a relation, closed form. (Contributed by AV, 20-Aug-2022.)
⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴𝑅𝑥)
Theorem	brimralrspcev 5173*	Restricted existential specialization with a restricted universal quantifier over an implication with a relation in the antecedent, closed form. (Contributed by AV, 20-Aug-2022.)
⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 ((𝜑 ∧ 𝐴𝑅𝐵) → 𝜓)) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝜑 ∧ 𝐴𝑅𝑥) → 𝜓))
2.1.24  Ordered-pair class abstractions (class builders)
Syntax	copab 5174	Extend class notation to include ordered-pair class abstraction (class builder).
class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
Definition	df-opab 5175*	Define the class abstraction of a collection of ordered pairs. Definition 3.3 of [Monk1] p. 34. Usually 𝑥 and 𝑦 are distinct, although the definition does not require it (see dfid2 5560 for a case where they are not distinct). The brace notation is called "class abstraction" by Quine; it is also called "class builder" in the literature. An alternate definition using no existential quantifiers is shown by dfopab2 8050. An example is given by ex-opab 30764. (Contributed by NM, 4-Jul-1994.)
⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
Theorem	opabss 5176*	The collection of ordered pairs in a class is a subclass of it. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑅𝑦} ⊆ 𝑅
Theorem	opabbid 5177	Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 21-Feb-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜒})
Theorem	opabbidv 5178*	Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 15-May-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜒})
Theorem	opabbii 5179	Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓}
Theorem	nfopabd 5180*	Bound-variable hypothesis builder for class abstraction. Deduction form. (Contributed by Scott Fenton, 26-Oct-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑧𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑧{⟨𝑥, 𝑦⟩ ∣ 𝜓})
Theorem	nfopab 5181*	Bound-variable hypothesis builder for class abstraction. (Contributed by NM, 1-Sep-1999.) Remove disjoint variable conditions. (Revised by Andrew Salmon, 11-Jul-2011.) (Revised by Scott Fenton, 26-Oct-2024.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ Ⅎ𝑧{⟨𝑥, 𝑦⟩ ∣ 𝜑}
Theorem	nfopab1 5182	The first abstraction variable in an ordered-pair class abstraction is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}
Theorem	nfopab2 5183	The second abstraction variable in an ordered-pair class abstraction is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑦{⟨𝑥, 𝑦⟩ ∣ 𝜑}
Theorem	cbvopab 5184*	Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 14-Sep-2003.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑤⟩ ∣ 𝜓}
Theorem	cbvopabv 5185*	Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996.) Reduce axiom usage. (Revised by GG, 15-Oct-2024.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑤⟩ ∣ 𝜓}
Theorem	cbvopab1 5186*	Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 6-Oct-2004.) (Revised by Mario Carneiro, 14-Oct-2016.) Add disjoint variable condition to avoid ax-13 2404. See cbvopab1g 5187 for a less restrictive version requiring more axioms. (Revised by GG, 17-Jan-2024.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ 𝜓}
Theorem	cbvopab1g 5187*	Change first bound variable in an ordered-pair class abstraction, using explicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2404. See cbvopab1 5186 for a version with more disjoint variable conditions, but not requiring ax-13 2404. (Contributed by NM, 6-Oct-2004.) (Revised by Mario Carneiro, 14-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ 𝜓}
Theorem	cbvopab2 5188*	Change second bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 22-Aug-2013.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑧⟩ ∣ 𝜓}
Theorem	cbvopab1s 5189*	Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 31-Jul-2003.)
⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ [𝑧 / 𝑥]𝜑}
Theorem	cbvopab1v 5190*	Rule used to change the first bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 31-Jul-2003.) (Proof shortened by Eric Schmidt, 4-Apr-2007.) Reduce axiom usage. (Revised by GG, 17-Nov-2024.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ 𝜓}
Theorem	cbvopab2v 5191*	Rule used to change the second bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 2-Sep-1999.)
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑧⟩ ∣ 𝜓}
Theorem	unopab 5192	Union of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.)
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∨ 𝜓)}
2.1.25  Functions in maps-to notation
Syntax	cmpt 5193	Extend the definition of a class to include maps-to notation for defining a function via a rule.
class (𝑥 ∈ 𝐴 ↦ 𝐵)
Definition	df-mpt 5194*	Define maps-to notation for defining a function via a rule. Read as "the function which maps 𝑥 (in 𝐴) to 𝐵(𝑥)". The class expression 𝐵 is the value of the function at 𝑥 and normally contains the variable 𝑥. An example is the square function for complex numbers, (𝑥 ∈ ℂ ↦ (𝑥↑2)). Similar to the definition of mapping in [ChoquetDD] p. 2. (Contributed by NM, 17-Feb-2008.)
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
Theorem	mpteq12da 5195	An equality inference for the maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) Remove dependency on ax-10 2176. (Revised by SN, 11-Nov-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))
Theorem	mpteq12df 5196	An equality inference for the maps-to notation. Compare mpteq12dv 5199. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Mario Carneiro, 11-Dec-2016.) (Proof shortened by SN, 11-Nov-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))
Theorem	mpteq12f 5197	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ ((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))
Theorem	mpteq12dva 5198*	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.) Remove dependency on ax-10 2176, ax-12 2213. (Revised by SN, 11-Nov-2024.)
⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))
Theorem	mpteq12dv 5199*	An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.) Remove dependency on ax-10 2176, ax-12 2213. (Revised by SN and GG, 1-Dec-2023.)
⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))
Theorem	mpteq12 5200*	An equality theorem for the maps-to notation. (Contributed by NM, 16-Dec-2013.)
⊢ ((𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))