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	3brtr3d 5101	Substitution of equality into both sides of a binary relation. (Contributed by NM, 18-Oct-1999.)
⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐶𝑅𝐷)
Theorem	3brtr4d 5102	Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.)
⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐴)    &   ⊢ (𝜑 → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐶𝑅𝐷)
Theorem	3brtr3g 5103	Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.)
⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ (𝜑 → 𝐶𝑅𝐷)
Theorem	3brtr4g 5104	Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.)
⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ (𝜑 → 𝐶𝑅𝐷)
Theorem	eqbrtrid 5105	A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	eqbrtrrid 5106	A chained equality inference for a binary relation. (Contributed by NM, 17-Sep-2004.)
⊢ 𝐵 = 𝐴    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	breqtrid 5107	A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
⊢ 𝐴𝑅𝐵    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	breqtrrid 5108	A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
⊢ 𝐴𝑅𝐵    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	eqbrtrdi 5109	A chained equality inference for a binary relation. (Contributed by NM, 12-Oct-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐵𝑅𝐶    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	eqbrtrrdi 5110	A chained equality inference for a binary relation. (Contributed by NM, 4-Jan-2006.)
⊢ (𝜑 → 𝐵 = 𝐴)    &   ⊢ 𝐵𝑅𝐶    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	breqtrdi 5111	A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	breqtrrdi 5112	A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	ssbrd 5113	Deduction from a subclass relationship of binary relations. (Contributed by NM, 30-Apr-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷))
Theorem	ssbr 5114	Implication from a subclass relationship of binary relations. (Contributed by Peter Mazsa, 11-Nov-2019.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷))
Theorem	ssbri 5115	Inference from a subclass relationship of binary relations. (Contributed by NM, 28-Mar-2007.) (Revised by Mario Carneiro, 8-Feb-2015.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ (𝐶𝐴𝐷 → 𝐶𝐵𝐷)
Theorem	nfbrd 5116	Deduction version of bound-variable hypothesis builder nfbr 5117. (Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝑅)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 𝐴𝑅𝐵)
Theorem	nfbr 5117	Bound-variable hypothesis builder for binary relation. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴𝑅𝐵
Theorem	brab1 5118*	Relationship between a binary relation and a class abstraction. (Contributed by Andrew Salmon, 8-Jul-2011.)
⊢ (𝑥𝑅𝐴 ↔ 𝑥 ∈ {𝑧 ∣ 𝑧𝑅𝐴})
Theorem	br0 5119	The empty binary relation never holds. (Contributed by NM, 23-Aug-2018.)
⊢ ¬ 𝐴∅𝐵
Theorem	brne0 5120	If two sets are in a binary relation, the relation cannot be empty. (Contributed by Alexander van der Vekens, 7-Jul-2018.)
⊢ (𝐴𝑅𝐵 → 𝑅 ≠ ∅)
Theorem	brun 5121	The union of two binary relations. (Contributed by NM, 21-Dec-2008.)
⊢ (𝐴(𝑅 ∪ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∨ 𝐴𝑆𝐵))
Theorem	brin 5122	The intersection of two relations. (Contributed by FL, 7-Oct-2008.)
⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵))
Theorem	brdif 5123	The difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2011.)
⊢ (𝐴(𝑅 ∖ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵))
Theorem	sbcbr123 5124	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) (Revised by NM, 22-Aug-2018.)
⊢ ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵⦋𝐴 / 𝑥⦌𝑅⦋𝐴 / 𝑥⦌𝐶)
Theorem	sbcbr 5125*	Move substitution in and out of a binary relation. (Contributed by NM, 23-Aug-2018.)
⊢ ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ 𝐵⦋𝐴 / 𝑥⦌𝑅𝐶)
Theorem	sbcbr12g 5126*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵𝑅⦋𝐴 / 𝑥⦌𝐶))
Theorem	sbcbr1g 5127*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵𝑅𝐶))
Theorem	sbcbr2g 5128*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ 𝐵𝑅⦋𝐴 / 𝑥⦌𝐶))
Theorem	brsymdif 5129	Characterization of the symmetric difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ (𝐴(𝑅 △ 𝑆)𝐵 ↔ ¬ (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵))
Theorem	brralrspcev 5130*	Restricted existential specialization with a restricted universal quantifier over a relation, closed form. (Contributed by AV, 20-Aug-2022.)
⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴𝑅𝑥)
Theorem	brimralrspcev 5131*	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 5132	Extend class notation to include ordered-pair class abstraction (class builder).
class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
Definition	df-opab 5133*	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 5482 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 7865. An example is given by ex-opab 28697. (Contributed by NM, 4-Jul-1994.)
⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
Theorem	opabss 5134*	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 5135	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 5136*	Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 15-May-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜒})
Theorem	opabbii 5137	Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓}
Theorem	nfopabd 5138*	Bound-variable hypothesis builder for class abstraction. Deduction form. (Contributed by Scott Fenton, 26-Oct-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑧𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑧{⟨𝑥, 𝑦⟩ ∣ 𝜓})
Theorem	nfopab 5139*	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 5140	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 5141	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 5142*	Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 14-Sep-2003.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑤⟩ ∣ 𝜓}
Theorem	cbvopabv 5143*	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 Gino Giotto, 15-Oct-2024.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑤⟩ ∣ 𝜓}
Theorem	cbvopabvOLD 5144*	Obsolete version of cbvopabv 5143 as of 15-Oct-2024. (Contributed by NM, 15-Oct-1996.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑤⟩ ∣ 𝜓}
Theorem	cbvopab1 5145*	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 2372. See cbvopab1g 5146 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 17-Jan-2024.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ 𝜓}
Theorem	cbvopab1g 5146*	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 2372. See cbvopab1 5145 for a version with more disjoint variable conditions, but not requiring ax-13 2372. (Contributed by NM, 6-Oct-2004.) (Revised by Mario Carneiro, 14-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ 𝜓}
Theorem	cbvopab2 5147*	Change second bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 22-Aug-2013.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑧⟩ ∣ 𝜓}
Theorem	cbvopab1s 5148*	Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 31-Jul-2003.)
⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ [𝑧 / 𝑥]𝜑}
Theorem	cbvopab1v 5149*	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 Gino Giotto, 17-Nov-2024.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ 𝜓}
Theorem	cbvopab1vOLD 5150*	Obsolete version of cbvopab1v 5149 as of 17-Nov-2024. (Contributed by NM, 31-Jul-2003.) (Proof shortened by Eric Schmidt, 4-Apr-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ 𝜓}
Theorem	cbvopab2v 5151*	Rule used to change the second bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 2-Sep-1999.)
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑧⟩ ∣ 𝜓}
Theorem	unopab 5152	Union of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.)
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∨ 𝜓)}
2.1.25  Functions in maps-to notation
Syntax	cmpt 5153	Extend the definition of a class to include maps-to notation for defining a function via a rule.
class (𝑥 ∈ 𝐴 ↦ 𝐵)
Definition	df-mpt 5154*	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 5155	An equality inference for the maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) Remove dependency on ax-10 2139. (Revised by SN, 11-Nov-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))
Theorem	mpteq12df 5156	An equality inference for the maps-to notation. Compare mpteq12dv 5161. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Mario Carneiro, 11-Dec-2016.) (Proof shortened by SN, 11-Nov-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))
Theorem	mpteq12dfOLD 5157	Obsolete version of mpteq12df 5156 as of 11-Nov-2024. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Mario Carneiro, 11-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))
Theorem	mpteq12f 5158	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ ((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))
Theorem	mpteq12dva 5159*	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.) Remove dependency on ax-10 2139, ax-12 2173. (Revised by SN, 11-Nov-2024.)
⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))
Theorem	mpteq12dvaOLD 5160*	Obsolete version of mpteq12dva 5159 as of 11-Nov-2024. (Contributed by Mario Carneiro, 26-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))
Theorem	mpteq12dv 5161*	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 2139, ax-12 2173. (Revised by SN and Gino Giotto, 1-Dec-2023.)
⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))
Theorem	mpteq12 5162*	An equality theorem for the maps-to notation. (Contributed by NM, 16-Dec-2013.)
⊢ ((𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))
Theorem	mpteq1 5163*	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Proof shortened by SN, 11-Nov-2024.)
⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	mpteq1OLD 5164*	Obsolete version of mpteq1 5163 as of 11-Nov-2024. (Contributed by Mario Carneiro, 16-Dec-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	mpteq1d 5165*	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 11-Jun-2016.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	mpteq1i 5166	An equality theorem for the maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.) Remove all disjoint variable conditions. (Revised by SN, 11-Nov-2024.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)
Theorem	mpteq1iOLD 5167*	An equality theorem for the maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)
Theorem	mpteq2da 5168	Slightly more general equality inference for the maps-to notation. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.) (Proof shortened by SN, 11-Nov-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
Theorem	mpteq2daOLD 5169	Obsolete version of mpteq2da 5168 as of 11-Nov-2024. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
Theorem	mpteq2dva 5170*	Slightly more general equality inference for the maps-to notation. (Contributed by Scott Fenton, 25-Apr-2012.) Remove dependency on ax-10 2139. (Revised by SN, 11-Nov-2024.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
Theorem	mpteq2dvaOLD 5171*	Obsolete version of mpteq2dva 5170 as of 11-Nov-2024. (Contributed by Scott Fenton, 25-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
Theorem	mpteq2dv 5172*	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 23-Aug-2014.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
Theorem	mpteq2ia 5173	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Proof shortened by SN, 11-Nov-2024.)
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)
Theorem	mpteq2iaOLD 5174	Obsolete version of mpteq2ia 5173 as of 11-Nov-2024. (Contributed by Mario Carneiro, 16-Dec-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)
Theorem	mpteq2i 5175	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)
Theorem	mpteq12i 5176	An equality inference for the maps-to notation. (Contributed by Scott Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.)
⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)
Theorem	nfmpt 5177*	Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵)
Theorem	nfmpt1 5178	Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.)
⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵)
Theorem	cbvmptf 5179*	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.) (Revised by Thierry Arnoux, 9-Mar-2017.) Add disjoint variable condition to avoid ax-13 2372. See cbvmptfg 5180 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 17-Jan-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)
Theorem	cbvmptfg 5180	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. Usage of this theorem is discouraged because it depends on ax-13 2372. See cbvmptf 5179 for a version with more disjoint variable conditions, but not requiring ax-13 2372. (Contributed by NM, 11-Sep-2011.) (Revised by Thierry Arnoux, 9-Mar-2017.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)
Theorem	cbvmpt 5181*	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.) Add disjoint variable condition to avoid ax-13 2372. See cbvmptg 5182 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 17-Jan-2024.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)
Theorem	cbvmptg 5182*	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. Usage of this theorem is discouraged because it depends on ax-13 2372. See cbvmpt 5181 for a version with more disjoint variable conditions, but not requiring ax-13 2372. (Contributed by NM, 11-Sep-2011.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)
Theorem	cbvmptv 5183*	Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.) Add disjoint variable condition to avoid auxiliary axioms . See cbvmptvg 5185 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 17-Nov-2024.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)
Theorem	cbvmptvOLD 5184*	Obsolete version of cbvmptv 5183 as of 17-Nov-2024. (Contributed by Mario Carneiro, 19-Feb-2013.) Add disjoint variable condition to avoid ax-13 2372. See cbvmptvg 5185 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 17-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)
Theorem	cbvmptvg 5185*	Rule to change the bound variable in a maps-to function, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2372. See cbvmptv 5183 for a version with more disjoint variable conditions, but not requiring ax-13 2372. (Contributed by Mario Carneiro, 19-Feb-2013.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)
Theorem	mptv 5186*	Function with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.)
⊢ (𝑥 ∈ V ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ 𝑦 = 𝐵}
2.1.26  Transitive classes
Syntax	wtr 5187	Extend wff notation to include transitive classes. Notation from [TakeutiZaring] p. 35.
wff Tr 𝐴
Definition	df-tr 5188	Define the transitive class predicate. Not to be confused with a transitive relation (see cotr 6006). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 5189 (which is suggestive of the word "transitive"), dftr3 5191, dftr4 5192, dftr5 5190, and (when 𝐴 is a set) unisuc 6327. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130. (Contributed by NM, 29-Aug-1993.)
⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)
Theorem	dftr2 5189*	An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40. (Contributed by NM, 24-Apr-1994.)
⊢ (Tr 𝐴 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴))
Theorem	dftr5 5190*	An alternate way of defining a transitive class. (Contributed by NM, 20-Mar-2004.)
⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 𝑦 ∈ 𝐴)
Theorem	dftr3 5191*	An alternate way of defining a transitive class. Definition 7.1 of [TakeutiZaring] p. 35. (Contributed by NM, 29-Aug-1993.)
⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴)
Theorem	dftr4 5192	An alternate way of defining a transitive class. Definition of [Enderton] p. 71. (Contributed by NM, 29-Aug-1993.)
⊢ (Tr 𝐴 ↔ 𝐴 ⊆ 𝒫 𝐴)
Theorem	treq 5193	Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.)
⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))
Theorem	trel 5194	In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (Tr 𝐴 → ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → 𝐵 ∈ 𝐴))
Theorem	trel3 5195	In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.)
⊢ (Tr 𝐴 → ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐷 ∧ 𝐷 ∈ 𝐴) → 𝐵 ∈ 𝐴))
Theorem	trss 5196	An element of a transitive class is a subset of the class. (Contributed by NM, 7-Aug-1994.) (Proof shortened by JJ, 26-Jul-2021.)
⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
Theorem	trin 5197	The intersection of transitive classes is transitive. (Contributed by NM, 9-May-1994.)
⊢ ((Tr 𝐴 ∧ Tr 𝐵) → Tr (𝐴 ∩ 𝐵))
Theorem	tr0 5198	The empty set is transitive. (Contributed by NM, 16-Sep-1993.)
⊢ Tr ∅
Theorem	trv 5199	The universe is transitive. (Contributed by NM, 14-Sep-2003.)
⊢ Tr V
Theorem	triun 5200	An indexed union of a class of transitive sets is transitive. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (∀𝑥 ∈ 𝐴 Tr 𝐵 → Tr ∪ 𝑥 ∈ 𝐴 𝐵)