P. 41 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4001-4100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sndisj 4001	Any collection of singletons is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Disj 𝑥 ∈ 𝐴 {𝑥}
Theorem	0disj 4002	Any collection of empty sets is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Disj 𝑥 ∈ 𝐴 ∅
Theorem	disjxsn 4003*	A singleton collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Disj 𝑥 ∈ {𝐴}𝐵
Theorem	disjx0 4004	An empty collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Disj 𝑥 ∈ ∅ 𝐵
2.1.22  Binary relations
Syntax	wbr 4005	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 𝐴𝑅𝐵
Definition	df-br 4006	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. 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 4897). (Contributed by NM, 31-Dec-1993.)
⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
Theorem	breq 4007	Equality theorem for binary relations. (Contributed by NM, 4-Jun-1995.)
⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵))
Theorem	breq1 4008	Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
Theorem	breq2 4009	Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))
Theorem	breq12 4010	Equality theorem for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
Theorem	breqi 4011	Equality inference for binary relations. (Contributed by NM, 19-Feb-2005.)
⊢ 𝑅 = 𝑆    ⇒   ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)
Theorem	breq1i 4012	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)
Theorem	breq2i 4013	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵)
Theorem	breq12i 4014	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)
Theorem	breq1d 4015	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
Theorem	breqd 4016	Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷))
Theorem	breq2d 4017	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))
Theorem	breq12d 4018	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
Theorem	breq123d 4019	Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝑅 = 𝑆)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑆𝐷))
Theorem	breqdi 4020	Equality deduction for a binary relation. (Contributed by Thierry Arnoux, 5-Oct-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶𝐴𝐷)    ⇒   ⊢ (𝜑 → 𝐶𝐵𝐷)
Theorem	breqan12d 4021	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
Theorem	breqan12rd 4022	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
Theorem	eqnbrtrd 4023	Substitution of equal classes into the negation of a binary relation. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → ¬ 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → ¬ 𝐴𝑅𝐶)
Theorem	nbrne1 4024	Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.)
⊢ ((𝐴𝑅𝐵 ∧ ¬ 𝐴𝑅𝐶) → 𝐵 ≠ 𝐶)
Theorem	nbrne2 4025	Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.)
⊢ ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴 ≠ 𝐵)
Theorem	eqbrtri 4026	Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵𝑅𝐶    ⇒   ⊢ 𝐴𝑅𝐶
Theorem	eqbrtrd 4027	Substitution of equal classes into a binary relation. (Contributed by NM, 8-Oct-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	eqbrtrri 4028	Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐴𝑅𝐶    ⇒   ⊢ 𝐵𝑅𝐶
Theorem	eqbrtrrd 4029	Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐵𝑅𝐶)
Theorem	breqtri 4030	Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴𝑅𝐵    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ 𝐴𝑅𝐶
Theorem	breqtrd 4031	Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	breqtrri 4032	Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴𝑅𝐵    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ 𝐴𝑅𝐶
Theorem	breqtrrd 4033	Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	3brtr3i 4034	Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.)
⊢ 𝐴𝑅𝐵    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ 𝐶𝑅𝐷
Theorem	3brtr4i 4035	Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.)
⊢ 𝐴𝑅𝐵    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ 𝐶𝑅𝐷
Theorem	3brtr3d 4036	Substitution of equality into both sides of a binary relation. (Contributed by NM, 18-Oct-1999.)
⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐶𝑅𝐷)
Theorem	3brtr4d 4037	Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.)
⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐴)    &   ⊢ (𝜑 → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐶𝑅𝐷)
Theorem	3brtr3g 4038	Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.)
⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ (𝜑 → 𝐶𝑅𝐷)
Theorem	3brtr4g 4039	Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.)
⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ (𝜑 → 𝐶𝑅𝐷)
Theorem	eqbrtrid 4040	B chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	eqbrtrrid 4041	B chained equality inference for a binary relation. (Contributed by NM, 17-Sep-2004.)
⊢ 𝐵 = 𝐴    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	breqtrid 4042	B chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
⊢ 𝐴𝑅𝐵    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	breqtrrid 4043	B chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
⊢ 𝐴𝑅𝐵    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	eqbrtrdi 4044	A chained equality inference for a binary relation. (Contributed by NM, 12-Oct-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐵𝑅𝐶    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	eqbrtrrdi 4045	A chained equality inference for a binary relation. (Contributed by NM, 4-Jan-2006.)
⊢ (𝜑 → 𝐵 = 𝐴)    &   ⊢ 𝐵𝑅𝐶    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	breqtrdi 4046	A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	breqtrrdi 4047	A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	ssbrd 4048	Deduction from a subclass relationship of binary relations. (Contributed by NM, 30-Apr-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷))
Theorem	ssbri 4049	Inference from a subclass relationship of binary relations. (Contributed by NM, 28-Mar-2007.) (Revised by Mario Carneiro, 8-Feb-2015.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ (𝐶𝐴𝐷 → 𝐶𝐵𝐷)
Theorem	nfbrd 4050	Deduction version of bound-variable hypothesis builder nfbr 4051. (Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝑅)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 𝐴𝑅𝐵)
Theorem	nfbr 4051	Bound-variable hypothesis builder for binary relation. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴𝑅𝐵
Theorem	brab1 4052*	Relationship between a binary relation and a class abstraction. (Contributed by Andrew Salmon, 8-Jul-2011.)
⊢ (𝑥𝑅𝐴 ↔ 𝑥 ∈ {𝑧 ∣ 𝑧𝑅𝐴})
Theorem	br0 4053	The empty binary relation never holds. (Contributed by NM, 23-Aug-2018.)
⊢ ¬ 𝐴∅𝐵
Theorem	brne0 4054	If two sets are in a binary relation, the relation cannot be empty. In fact, the relation is also inhabited, as seen at brm 4055. (Contributed by Alexander van der Vekens, 7-Jul-2018.)
⊢ (𝐴𝑅𝐵 → 𝑅 ≠ ∅)
Theorem	brm 4055*	If two sets are in a binary relation, the relation is inhabited. (Contributed by Jim Kingdon, 31-Dec-2023.)
⊢ (𝐴𝑅𝐵 → ∃𝑥 𝑥 ∈ 𝑅)
Theorem	brun 4056	The union of two binary relations. (Contributed by NM, 21-Dec-2008.)
⊢ (𝐴(𝑅 ∪ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∨ 𝐴𝑆𝐵))
Theorem	brin 4057	The intersection of two relations. (Contributed by FL, 7-Oct-2008.)
⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵))
Theorem	brdif 4058	The difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2011.)
⊢ (𝐴(𝑅 ∖ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵))
Theorem	sbcbrg 4059	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵⦋𝐴 / 𝑥⦌𝑅⦋𝐴 / 𝑥⦌𝐶))
Theorem	sbcbr12g 4060*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵𝑅⦋𝐴 / 𝑥⦌𝐶))
Theorem	sbcbr1g 4061*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵𝑅𝐶))
Theorem	sbcbr2g 4062*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ 𝐵𝑅⦋𝐴 / 𝑥⦌𝐶))
Theorem	brralrspcev 4063*	Restricted existential specialization with a restricted universal quantifier over a relation, closed form. (Contributed by AV, 20-Aug-2022.)
⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴𝑅𝑥)
Theorem	brimralrspcev 4064*	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.23  Ordered-pair class abstractions (class builders)
Syntax	copab 4065	Extend class notation to include ordered-pair class abstraction (class builder).
class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
Syntax	cmpt 4066	Extend the definition of a class to include maps-to notation for defining a function via a rule.
class (𝑥 ∈ 𝐴 ↦ 𝐵)
Definition	df-opab 4067*	Define the class abstraction of a collection of ordered pairs. Definition 3.3 of [Monk1] p. 34. Usually 𝑥 and 𝑦 are distinct, although the definition doesn't strictly require it. The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. (Contributed by NM, 4-Jul-1994.)
⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
Definition	df-mpt 4068*	Define maps-to notation for defining a function via a rule. Read as "the function defined by the map from 𝑥 (in 𝐴) to 𝐵(𝑥)". The class expression 𝐵 is the value of the function at 𝑥 and normally contains the variable 𝑥. Similar to the definition of mapping in [ChoquetDD] p. 2. (Contributed by NM, 17-Feb-2008.)
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
Theorem	opabss 4069*	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 4070	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 4071*	Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 15-May-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜒})
Theorem	opabbii 4072	Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓}
Theorem	nfopab 4073*	Bound-variable hypothesis builder for class abstraction. (Contributed by NM, 1-Sep-1999.) Remove disjoint variable conditions. (Revised by Andrew Salmon, 11-Jul-2011.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ Ⅎ𝑧{⟨𝑥, 𝑦⟩ ∣ 𝜑}
Theorem	nfopab1 4074	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.)
⊢ Ⅎ𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}
Theorem	nfopab2 4075	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.)
⊢ Ⅎ𝑦{⟨𝑥, 𝑦⟩ ∣ 𝜑}
Theorem	cbvopab 4076*	Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 14-Sep-2003.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑤⟩ ∣ 𝜓}
Theorem	cbvopabv 4077*	Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑤⟩ ∣ 𝜓}
Theorem	cbvopab1 4078*	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.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ 𝜓}
Theorem	cbvopab2 4079*	Change second bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 22-Aug-2013.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑧⟩ ∣ 𝜓}
Theorem	cbvopab1s 4080*	Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 31-Jul-2003.)
⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ [𝑧 / 𝑥]𝜑}
Theorem	cbvopab1v 4081*	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.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ 𝜓}
Theorem	cbvopab2v 4082*	Rule used to change the second bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 2-Sep-1999.)
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑧⟩ ∣ 𝜓}
Theorem	csbopabg 4083*	Move substitution into a class abstraction. (Contributed by NM, 6-Aug-2007.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{⟨𝑦, 𝑧⟩ ∣ 𝜑} = {⟨𝑦, 𝑧⟩ ∣ [𝐴 / 𝑥]𝜑})
Theorem	unopab 4084	Union of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.)
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∨ 𝜓)}
Theorem	mpteq12f 4085	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ ((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))
Theorem	mpteq12dva 4086*	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))
Theorem	mpteq12dv 4087*	An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.)
⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))
Theorem	mpteq12 4088*	An equality theorem for the maps-to notation. (Contributed by NM, 16-Dec-2013.)
⊢ ((𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))
Theorem	mpteq1 4089*	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	mpteq1d 4090*	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 11-Jun-2016.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	mpteq2ia 4091	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)
Theorem	mpteq2i 4092	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)
Theorem	mpteq12i 4093	An equality inference for the maps-to notation. (Contributed by Scott Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.)
⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)
Theorem	mpteq2da 4094	Slightly more general equality inference for the maps-to notation. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
Theorem	mpteq2dva 4095*	Slightly more general equality inference for the maps-to notation. (Contributed by Scott Fenton, 25-Apr-2012.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
Theorem	mpteq2dv 4096*	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 23-Aug-2014.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
Theorem	nfmpt 4097*	Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵)
Theorem	nfmpt1 4098	Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.)
⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵)
Theorem	cbvmptf 4099*	Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by Thierry Arnoux, 9-Mar-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)
Theorem	cbvmpt 4100*	Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 11-Sep-2011.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)