P. 47 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 4601-4700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	proj1op 4601	The first projection operator applied to an ordered pair yields its first member. Theorem X.2.7 of [Rosser] p. 282. (Contributed by SF, 3-Feb-2015.)
⊢ Proj1 ⟨A, B⟩ = A
Theorem	proj2op 4602	The second projection operator applied to an ordered pair yields its second member. Theorem X.2.8 of [Rosser] p. 283. (Contributed by SF, 3-Feb-2015.)
⊢ Proj2 ⟨A, B⟩ = B
Theorem	opth 4603	The ordered pair theorem. Two ordered pairs are equal iff their components are equal. (Contributed by SF, 2-Jan-2015.)
⊢ (⟨A, B⟩ = ⟨C, D⟩ ↔ (A = C ∧ B = D))
Theorem	opexb 4604	An ordered pair is a set iff its components are sets. (Contributed by SF, 2-Jan-2015.)
⊢ (⟨A, B⟩ ∈ V ↔ (A ∈ V ∧ B ∈ V))
Theorem	nfop 4605	Bound-variable hypothesis builder for ordered pairs. (Contributed by SF, 2-Jan-2015.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx⟨A, B⟩
Theorem	nfopd 4606	Deduction version of bound-variable hypothesis builder nfop 4605. (Contributed by SF, 2-Jan-2015.)
⊢ (φ → ℲxA)    &   ⊢ (φ → ℲxB)    ⇒   ⊢ (φ → Ⅎx⟨A, B⟩)
Theorem	eqvinop 4607*	A variable introduction law for ordered pairs. Analog of Lemma 15 of [Monk2] p. 109. (Contributed by NM, 28-May-1995.)
⊢ B ∈ V    &   ⊢ C ∈ V    ⇒   ⊢ (A = ⟨B, C⟩ ↔ ∃x∃y(A = ⟨x, y⟩ ∧ ⟨x, y⟩ = ⟨B, C⟩))
Theorem	copsexg 4608*	Substitution of class A for ordered pair ⟨x, y⟩. (Contributed by NM, 27-Dec-1996.) (Revised by Andrew Salmon, 25-Jul-2011.)
⊢ (A = ⟨x, y⟩ → (φ ↔ ∃x∃y(A = ⟨x, y⟩ ∧ φ)))
Theorem	copsex2t 4609*	Closed theorem form of copsex2g 4610. (Contributed by NM, 17-Feb-2013.)
⊢ ((∀x∀y((x = A ∧ y = B) → (φ ↔ ψ)) ∧ (A ∈ V ∧ B ∈ W)) → (∃x∃y(⟨A, B⟩ = ⟨x, y⟩ ∧ φ) ↔ ψ))
Theorem	copsex2g 4610*	Implicit substitution inference for ordered pairs. (Contributed by NM, 28-May-1995.)
⊢ ((x = A ∧ y = B) → (φ ↔ ψ))    ⇒   ⊢ ((A ∈ V ∧ B ∈ W) → (∃x∃y(⟨A, B⟩ = ⟨x, y⟩ ∧ φ) ↔ ψ))
Theorem	copsex4g 4611*	An implicit substitution inference for 2 ordered pairs. (Contributed by NM, 5-Aug-1995.)
⊢ (((x = A ∧ y = B) ∧ (z = C ∧ w = D)) → (φ ↔ ψ))    ⇒   ⊢ (((A ∈ R ∧ B ∈ S) ∧ (C ∈ R ∧ D ∈ S)) → (∃x∃y∃z∃w((⟨A, B⟩ = ⟨x, y⟩ ∧ ⟨C, D⟩ = ⟨z, w⟩) ∧ φ) ↔ ψ))
Theorem	eqop 4612*	Express equality to an ordered pair. (Contributed by SF, 6-Jan-2015.)
⊢ (A = ⟨B, C⟩ ↔ ∀z(z ∈ A ↔ (∃t ∈ B z = Phi t ∨ ∃t ∈ C z = ( Phi t ∪ {0c}))))
Theorem	mosubopt 4613*	"At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-Aug-2007.)
⊢ (∀y∀z∃*xφ → ∃*x∃y∃z(A = ⟨y, z⟩ ∧ φ))
Theorem	mosubop 4614*	"At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-May-1995.)
⊢ ∃*xφ    ⇒   ⊢ ∃*x∃y∃z(A = ⟨y, z⟩ ∧ φ)
Theorem	phiun 4615	The phi operation distributes over union. (Contributed by SF, 20-Feb-2015.)
⊢ Phi (A ∪ B) = ( Phi A ∪ Phi B)
Theorem	phidisjnn 4616	The phi operation applied to a set disjoint from the naturals has no effect. (Contributed by SF, 20-Feb-2015.)
⊢ ((A ∩ Nn ) = ∅ → Phi A = A)
Theorem	phialllem1 4617*	Lemma for phiall 4619. Any set of numbers without zero is the Phi of a set. (Contributed by Scott Fenton, 14-Apr-2021.)
⊢ A ∈ V    ⇒   ⊢ ((A ⊆ Nn ∧ ¬ 0c ∈ A) → ∃x A = Phi x)
Theorem	phialllem2 4618*	Lemma for phiall 4619. Any set without 0c is equal to the Phi of a set. (Contributed by Scott Fenton, 8-Apr-2021.)
⊢ A ∈ V    ⇒   ⊢ (¬ 0c ∈ A → ∃x A = Phi x)
Theorem	phiall 4619*	Any set is equal to either the Phi of another set or to a Phi with 0c adjoined. (Contributed by Scott Fenton, 8-Apr-2021.)
⊢ A ∈ V    ⇒   ⊢ ∃x(A = Phi x ∨ A = ( Phi x ∪ {0c}))
Theorem	opeq 4620	Any class is equal to an ordered pair. (Contributed by Scott Fenton, 8-Apr-2021.)
⊢ A = ⟨ Proj1 A, Proj2 A⟩
Theorem	opeqexb 4621*	A class is a set iff it is equal to an ordered pair. (Contributed by Scott Fenton, 19-Apr-2021.)
⊢ (A ∈ V ↔ ∃x∃y A = ⟨x, y⟩)
Theorem	opeqex 4622*	Any set is equal to some ordered pair. (Contributed by Scott Fenton, 16-Apr-2021.)
⊢ (A ∈ V → ∃x∃y A = ⟨x, y⟩)
2.3.2  Ordered-pair class abstractions (class builders)
Syntax	copab 4623	Extend class notation to include ordered-pair class abstraction (class builder).
class {⟨x, y⟩ ∣ φ}
Definition	df-opab 4624*	Define the class abstraction of a collection of ordered pairs. Definition 3.3 of [Monk1] p. 34. Usually x and y are distinct, although the definition doesn't strictly require it (see dfid2 4770 for a case where they are not distinct). The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. (Contributed by SF, 12-Jan-2015.)
⊢ {⟨x, y⟩ ∣ φ} = {z ∣ ∃x∃y(z = ⟨x, y⟩ ∧ φ)}
Theorem	opabbid 4625	Equivalent wff's yield equal ordered-pair class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ Ⅎxφ    &   ⊢ Ⅎyφ    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → {⟨x, y⟩ ∣ ψ} = {⟨x, y⟩ ∣ χ})
Theorem	opabbidv 4626*	Equivalent wff's yield equal ordered-pair class abstractions (deduction rule). (Contributed by NM, 15-May-1995.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → {⟨x, y⟩ ∣ ψ} = {⟨x, y⟩ ∣ χ})
Theorem	opabbii 4627	Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.)
⊢ (φ ↔ ψ)    ⇒   ⊢ {⟨x, y⟩ ∣ φ} = {⟨x, y⟩ ∣ ψ}
Theorem	nfopab 4628*	Bound-variable hypothesis builder for class abstraction. (Contributed by NM, 1-Sep-1999.) (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 11-Jul-2011.)
⊢ Ⅎzφ    ⇒   ⊢ Ⅎz{⟨x, y⟩ ∣ φ}
Theorem	nfopab1 4629	The first abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎx{⟨x, y⟩ ∣ φ}
Theorem	nfopab2 4630	The second abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎy{⟨x, y⟩ ∣ φ}
Theorem	cbvopab 4631*	Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 14-Sep-2003.)
⊢ Ⅎzφ    &   ⊢ Ⅎwφ    &   ⊢ Ⅎxψ    &   ⊢ Ⅎyψ    &   ⊢ ((x = z ∧ y = w) → (φ ↔ ψ))    ⇒   ⊢ {⟨x, y⟩ ∣ φ} = {⟨z, w⟩ ∣ ψ}
Theorem	cbvopabv 4632*	Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996.)
⊢ ((x = z ∧ y = w) → (φ ↔ ψ))    ⇒   ⊢ {⟨x, y⟩ ∣ φ} = {⟨z, w⟩ ∣ ψ}
Theorem	cbvopab1 4633*	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.)
⊢ Ⅎzφ    &   ⊢ Ⅎxψ    &   ⊢ (x = z → (φ ↔ ψ))    ⇒   ⊢ {⟨x, y⟩ ∣ φ} = {⟨z, y⟩ ∣ ψ}
Theorem	cbvopab2 4634*	Change second bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 22-Aug-2013.)
⊢ Ⅎzφ    &   ⊢ Ⅎyψ    &   ⊢ (y = z → (φ ↔ ψ))    ⇒   ⊢ {⟨x, y⟩ ∣ φ} = {⟨x, z⟩ ∣ ψ}
Theorem	cbvopab1s 4635*	Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 31-Jul-2003.)
⊢ {⟨x, y⟩ ∣ φ} = {⟨z, y⟩ ∣ [z / x]φ}
Theorem	cbvopab1v 4636*	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.)
⊢ (x = z → (φ ↔ ψ))    ⇒   ⊢ {⟨x, y⟩ ∣ φ} = {⟨z, y⟩ ∣ ψ}
Theorem	cbvopab2v 4637*	Rule used to change the second bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 2-Sep-1999.)
⊢ (y = z → (φ ↔ ψ))    ⇒   ⊢ {⟨x, y⟩ ∣ φ} = {⟨x, z⟩ ∣ ψ}
Theorem	csbopabg 4638*	Move substitution into a class abstraction. (Contributed by NM, 6-Aug-2007.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
⊢ (A ∈ V → [A / x]{⟨y, z⟩ ∣ φ} = {⟨y, z⟩ ∣ [̣A / x]̣φ})
Theorem	unopab 4639	Union of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.)
⊢ ({⟨x, y⟩ ∣ φ} ∪ {⟨x, y⟩ ∣ ψ}) = {⟨x, y⟩ ∣ (φ ∨ ψ)}
2.3.3  Binary relations
Syntax	wbr 4640	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.
wff ARB
Definition	df-br 4641	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 R normally denotes a relation that compares two classes A and B. This definition is well-defined, although not very meaningful, when classes A and/or B are proper classes (i.e. are not sets). On the other hand, we often find uses for this definition when R is a proper class. (Contributed by NM, 4-Jun-1995.)
⊢ (ARB ↔ ⟨A, B⟩ ∈ R)
Theorem	breq 4642	Equality theorem for binary relations. (Contributed by NM, 4-Jun-1995.)
⊢ (R = S → (ARB ↔ ASB))
Theorem	breq1 4643	Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
⊢ (A = B → (ARC ↔ BRC))
Theorem	breq2 4644	Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
⊢ (A = B → (CRA ↔ CRB))
Theorem	breq12 4645	Equality theorem for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ ((A = B ∧ C = D) → (ARC ↔ BRD))
Theorem	breqi 4646	Equality inference for binary relations. (Contributed by NM, 19-Feb-2005.)
⊢ R = S    ⇒   ⊢ (ARB ↔ ASB)
Theorem	breq1i 4647	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ A = B    ⇒   ⊢ (ARC ↔ BRC)
Theorem	breq2i 4648	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ A = B    ⇒   ⊢ (CRA ↔ CRB)
Theorem	breq12i 4649	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) (Revised by Eric Schmidt, 4-Apr-2007.)
⊢ A = B    &   ⊢ C = D    ⇒   ⊢ (ARC ↔ BRD)
Theorem	breq1d 4650	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (ARC ↔ BRC))
Theorem	breqd 4651	Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (CAD ↔ CBD))
Theorem	breq2d 4652	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (CRA ↔ CRB))
Theorem	breq12d 4653	Equality deduction for a binary relation. (The proof was shortened by Andrew Salmon, 9-Jul-2011.) (Contributed by NM, 8-Feb-1996.) (Revised by set.mm contributors, 9-Jul-2011.)
⊢ (φ → A = B)    &   ⊢ (φ → C = D)    ⇒   ⊢ (φ → (ARC ↔ BRD))
Theorem	breq123d 4654	Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)
⊢ (φ → A = B)    &   ⊢ (φ → R = S)    &   ⊢ (φ → C = D)    ⇒   ⊢ (φ → (ARC ↔ BSD))
Theorem	breqan12d 4655	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ (φ → A = B)    &   ⊢ (ψ → C = D)    ⇒   ⊢ ((φ ∧ ψ) → (ARC ↔ BRD))
Theorem	breqan12rd 4656	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ (φ → A = B)    &   ⊢ (ψ → C = D)    ⇒   ⊢ ((ψ ∧ φ) → (ARC ↔ BRD))
Theorem	nbrne1 4657	Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.)
⊢ ((ARB ∧ ¬ ARC) → B ≠ C)
Theorem	nbrne2 4658	Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.)
⊢ ((ARC ∧ ¬ BRC) → A ≠ B)
Theorem	eqbrtri 4659	Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
⊢ A = B    &   ⊢ BRC    ⇒   ⊢ ARC
Theorem	eqbrtrd 4660	Substitution of equal classes into a binary relation. (Contributed by NM, 8-Oct-1999.)
⊢ (φ → A = B)    &   ⊢ (φ → BRC)    ⇒   ⊢ (φ → ARC)
Theorem	eqbrtrri 4661	Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
⊢ A = B    &   ⊢ ARC    ⇒   ⊢ BRC
Theorem	eqbrtrrd 4662	Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
⊢ (φ → A = B)    &   ⊢ (φ → ARC)    ⇒   ⊢ (φ → BRC)
Theorem	breqtri 4663	Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
⊢ ARB    &   ⊢ B = C    ⇒   ⊢ ARC
Theorem	breqtrd 4664	Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
⊢ (φ → ARB)    &   ⊢ (φ → B = C)    ⇒   ⊢ (φ → ARC)
Theorem	breqtrri 4665	Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
⊢ ARB    &   ⊢ C = B    ⇒   ⊢ ARC
Theorem	breqtrrd 4666	Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
⊢ (φ → ARB)    &   ⊢ (φ → C = B)    ⇒   ⊢ (φ → ARC)
Theorem	3brtr3i 4667	Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.)
⊢ ARB    &   ⊢ A = C    &   ⊢ B = D    ⇒   ⊢ CRD
Theorem	3brtr4i 4668	Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.)
⊢ ARB    &   ⊢ C = A    &   ⊢ D = B    ⇒   ⊢ CRD
Theorem	3brtr3d 4669	Substitution of equality into both sides of a binary relation. (Contributed by NM, 18-Oct-1999.)
⊢ (φ → ARB)    &   ⊢ (φ → A = C)    &   ⊢ (φ → B = D)    ⇒   ⊢ (φ → CRD)
Theorem	3brtr4d 4670	Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.)
⊢ (φ → ARB)    &   ⊢ (φ → C = A)    &   ⊢ (φ → D = B)    ⇒   ⊢ (φ → CRD)
Theorem	3brtr3g 4671	Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.)
⊢ (φ → ARB)    &   ⊢ A = C    &   ⊢ B = D    ⇒   ⊢ (φ → CRD)
Theorem	3brtr4g 4672	Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.)
⊢ (φ → ARB)    &   ⊢ C = A    &   ⊢ D = B    ⇒   ⊢ (φ → CRD)
Theorem	syl5eqbr 4673	B chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
⊢ A = B    &   ⊢ (φ → BRC)    ⇒   ⊢ (φ → ARC)
Theorem	syl5eqbrr 4674	B chained equality inference for a binary relation. (Contributed by NM, 17-Sep-2004.)
⊢ B = A    &   ⊢ (φ → BRC)    ⇒   ⊢ (φ → ARC)
Theorem	syl5breq 4675	B chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
⊢ ARB    &   ⊢ (φ → B = C)    ⇒   ⊢ (φ → ARC)
Theorem	syl5breqr 4676	B chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
⊢ ARB    &   ⊢ (φ → C = B)    ⇒   ⊢ (φ → ARC)
Theorem	syl6eqbr 4677	A chained equality inference for a binary relation. (Contributed by NM, 12-Oct-1999.)
⊢ (φ → A = B)    &   ⊢ BRC    ⇒   ⊢ (φ → ARC)
Theorem	syl6eqbrr 4678	A chained equality inference for a binary relation. (Contributed by NM, 4-Jan-2006.)
⊢ (φ → B = A)    &   ⊢ BRC    ⇒   ⊢ (φ → ARC)
Theorem	syl6breq 4679	A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
⊢ (φ → ARB)    &   ⊢ B = C    ⇒   ⊢ (φ → ARC)
Theorem	syl6breqr 4680	A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
⊢ (φ → ARB)    &   ⊢ C = B    ⇒   ⊢ (φ → ARC)
Theorem	ssbrd 4681	Deduction from a subclass relationship of binary relations. (Contributed by NM, 30-Apr-2004.)
⊢ (φ → A ⊆ B)    ⇒   ⊢ (φ → (CAD → CBD))
Theorem	ssbri 4682	Inference from a subclass relationship of binary relations. (The proof was shortened by Andrew Salmon, 9-Jul-2011.) (Contributed by NM, 28-Mar-2007.) (Revised by set.mm contributors, 9-Jul-2011.)
⊢ A ⊆ B    ⇒   ⊢ (CAD → CBD)
Theorem	nfbrd 4683	Deduction version of bound-variable hypothesis builder nfbr 4684. (Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ (φ → ℲxA)    &   ⊢ (φ → ℲxR)    &   ⊢ (φ → ℲxB)    ⇒   ⊢ (φ → Ⅎx ARB)
Theorem	nfbr 4684	Bound-variable hypothesis builder for binary relation. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ ℲxA    &   ⊢ ℲxR    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx ARB
Theorem	brab1 4685*	Relationship between a binary relation and a class abstraction. (Contributed by Andrew Salmon, 8-Jul-2011.)
⊢ (xRA ↔ x ∈ {z ∣ zRA})
Theorem	sbcbrg 4686	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (A ∈ D → ([̣A / x]̣BRC ↔ [A / x]B[A / x]R[A / x]C))
Theorem	sbcbr12g 4687*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
⊢ (A ∈ D → ([̣A / x]̣BRC ↔ [A / x]BR[A / x]C))
Theorem	sbcbr1g 4688*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
⊢ (A ∈ D → ([̣A / x]̣BRC ↔ [A / x]BRC))
Theorem	sbcbr2g 4689*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
⊢ (A ∈ D → ([̣A / x]̣BRC ↔ BR[A / x]C))
Theorem	brex 4690	Binary relationship implies sethood of both parts. (Contributed by SF, 7-Jan-2015.)
⊢ (ARB → (A ∈ V ∧ B ∈ V))
Theorem	brreldmex 4691	Binary relationship implies sethood of domain. (Contributed by SF, 7-Jan-2018.)
⊢ (ARB → A ∈ V)
Theorem	brrelrnex 4692	Binary relationship implies sethood of range. (Contributed by SF, 7-Jan-2018.)
⊢ (ARB → B ∈ V)
Theorem	brun 4693	The union of two binary relations. (Contributed by NM, 21-Dec-2008.)
⊢ (A(R ∪ S)B ↔ (ARB ∨ ASB))
Theorem	brin 4694	The intersection of two relations. (Contributed by FL, 7-Oct-2008.)
⊢ (A(R ∩ S)B ↔ (ARB ∧ ASB))
Theorem	brdif 4695	The difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2011.)
⊢ (A(R ∖ S)B ↔ (ARB ∧ ¬ ASB))
2.3.4  Ordered-pair class abstractions (cont.)
Theorem	opabid 4696	The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. (The proof was shortened by Andrew Salmon, 25-Jul-2011.) (Contributed by NM, 14-Apr-1995.) (Revised by set.mm contributors, 25-Jul-2011.)
⊢ (⟨x, y⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ φ)
Theorem	elopab 4697*	Membership in a class abstraction of pairs. (Contributed by NM, 24-Mar-1998.)
⊢ (A ∈ {⟨x, y⟩ ∣ φ} ↔ ∃x∃y(A = ⟨x, y⟩ ∧ φ))
Theorem	opelopabsb 4698*	The law of concretion in terms of substitutions. (Contributed by NM, 30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.)
⊢ (⟨A, B⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ [̣A / x]̣[̣B / y]̣φ)
Theorem	brabsb 4699*	The law of concretion in terms of substitutions. (Contributed by NM, 17-Mar-2008.)
⊢ R = {⟨x, y⟩ ∣ φ}    ⇒   ⊢ (ARB ↔ [̣A / x]̣[̣B / y]̣φ)
Theorem	opelopabt 4700*	Closed theorem form of opelopab 4709. (Contributed by NM, 19-Feb-2013.)
⊢ ((∀x∀y(x = A → (φ ↔ ψ)) ∧ ∀x∀y(y = B → (ψ ↔ χ)) ∧ (A ∈ V ∧ B ∈ W)) → (⟨A, B⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ χ))