P. 42 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4101-4200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	eqbrtrdi 4101	A chained equality inference for a binary relation. (Contributed by NM, 12-Oct-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ 𝐵𝑅𝐶    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	eqbrtrrdi 4102	A chained equality inference for a binary relation. (Contributed by NM, 4-Jan-2006.)
⊢ (𝜑 → 𝐵 = 𝐴)    &   ⊢ 𝐵𝑅𝐶    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	breqtrdi 4103	A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	breqtrrdi 4104	A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	ssbrd 4105	Deduction from a subclass relationship of binary relations. (Contributed by NM, 30-Apr-2004.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷))
Theorem	ssbr 4106	Implication from a subclass relationship of binary relations. (Contributed by Peter Mazsa, 11-Nov-2019.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷))
Theorem	ssbri 4107	Inference from a subclass relationship of binary relations. (Contributed by NM, 28-Mar-2007.) (Revised by Mario Carneiro, 8-Feb-2015.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ (𝐶𝐴𝐷 → 𝐶𝐵𝐷)
Theorem	nfbrd 4108	Deduction version of bound-variable hypothesis builder nfbr 4109. (Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝑅)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 𝐴𝑅𝐵)
Theorem	nfbr 4109	Bound-variable hypothesis builder for binary relation. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴𝑅𝐵
Theorem	brab1 4110*	Relationship between a binary relation and a class abstraction. (Contributed by Andrew Salmon, 8-Jul-2011.)
⊢ (𝑥𝑅𝐴 ↔ 𝑥 ∈ {𝑧 ∣ 𝑧𝑅𝐴})
Theorem	br0 4111	The empty binary relation never holds. (Contributed by NM, 23-Aug-2018.)
⊢ ¬ 𝐴∅𝐵
Theorem	brne0 4112	If two sets are in a binary relation, the relation cannot be empty. In fact, the relation is also inhabited, as seen at brm 4113. (Contributed by Alexander van der Vekens, 7-Jul-2018.)
⊢ (𝐴𝑅𝐵 → 𝑅 ≠ ∅)
Theorem	brm 4113*	If two sets are in a binary relation, the relation is inhabited. (Contributed by Jim Kingdon, 31-Dec-2023.)
⊢ (𝐴𝑅𝐵 → ∃𝑥 𝑥 ∈ 𝑅)
Theorem	brun 4114	The union of two binary relations. (Contributed by NM, 21-Dec-2008.)
⊢ (𝐴(𝑅 ∪ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∨ 𝐴𝑆𝐵))
Theorem	brin 4115	The intersection of two relations. (Contributed by FL, 7-Oct-2008.)
⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵))
Theorem	brdif 4116	The difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2011.)
⊢ (𝐴(𝑅 ∖ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵))
Theorem	sbcbrg 4117	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 4118*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵𝑅⦋𝐴 / 𝑥⦌𝐶))
Theorem	sbcbr1g 4119*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵𝑅𝐶))
Theorem	sbcbr2g 4120*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ 𝐵𝑅⦋𝐴 / 𝑥⦌𝐶))
Theorem	brralrspcev 4121*	Restricted existential specialization with a restricted universal quantifier over a relation, closed form. (Contributed by AV, 20-Aug-2022.)
⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴𝑅𝑥)
Theorem	brimralrspcev 4122*	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 4123	Extend class notation to include ordered-pair class abstraction (class builder).
class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
Syntax	cmpt 4124	Extend the definition of a class to include maps-to notation for defining a function via a rule.
class (𝑥 ∈ 𝐴 ↦ 𝐵)
Definition	df-opab 4125*	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 4126*	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 4127*	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 4128	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 4129*	Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 15-May-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜒})
Theorem	opabbii 4130	Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓}
Theorem	nfopab 4131*	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 4132	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 4133	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 4134*	Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 14-Sep-2003.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑤⟩ ∣ 𝜓}
Theorem	cbvopabv 4135*	Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑤⟩ ∣ 𝜓}
Theorem	cbvopab1 4136*	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 4137*	Change second bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 22-Aug-2013.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑧⟩ ∣ 𝜓}
Theorem	cbvopab1s 4138*	Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 31-Jul-2003.)
⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ [𝑧 / 𝑥]𝜑}
Theorem	cbvopab1v 4139*	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 4140*	Rule used to change the second bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 2-Sep-1999.)
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑧⟩ ∣ 𝜓}
Theorem	csbopabg 4141*	Move substitution into a class abstraction. (Contributed by NM, 6-Aug-2007.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{⟨𝑦, 𝑧⟩ ∣ 𝜑} = {⟨𝑦, 𝑧⟩ ∣ [𝐴 / 𝑥]𝜑})
Theorem	unopab 4142	Union of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.)
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∨ 𝜓)}
Theorem	mpteq12f 4143	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ ((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))
Theorem	mpteq12dva 4144*	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))
Theorem	mpteq12dv 4145*	An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.)
⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))
Theorem	mpteq12 4146*	An equality theorem for the maps-to notation. (Contributed by NM, 16-Dec-2013.)
⊢ ((𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))
Theorem	mpteq1 4147*	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	mpteq1d 4148*	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 11-Jun-2016.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	mpteq2ia 4149	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)
Theorem	mpteq2i 4150	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)
Theorem	mpteq12i 4151	An equality inference for the maps-to notation. (Contributed by Scott Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.)
⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)
Theorem	mpteq2da 4152	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 4153*	Slightly more general equality inference for the maps-to notation. (Contributed by Scott Fenton, 25-Apr-2012.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
Theorem	mpteq2dv 4154*	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 23-Aug-2014.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
Theorem	nfmpt 4155*	Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵)
Theorem	nfmpt1 4156	Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.)
⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵)
Theorem	cbvmptf 4157*	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 4158*	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.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)
Theorem	cbvmptv 4159*	Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)
Theorem	mptv 4160*	Function with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.)
⊢ (𝑥 ∈ V ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ 𝑦 = 𝐵}
2.1.24  Transitive classes
Syntax	wtr 4161	Extend wff notation to include transitive classes. Notation from [TakeutiZaring] p. 35.
wff Tr 𝐴
Definition	df-tr 4162	Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4163 (which is suggestive of the word "transitive"), dftr3 4165, dftr4 4166, and dftr5 4164. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130. (Contributed by NM, 29-Aug-1993.)
⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)
Theorem	dftr2 4163*	An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40. (Contributed by NM, 24-Apr-1994.)
⊢ (Tr 𝐴 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴))
Theorem	dftr5 4164*	An alternate way of defining a transitive class. (Contributed by NM, 20-Mar-2004.)
⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 𝑦 ∈ 𝐴)
Theorem	dftr3 4165*	An alternate way of defining a transitive class. Definition 7.1 of [TakeutiZaring] p. 35. (Contributed by NM, 29-Aug-1993.)
⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴)
Theorem	dftr4 4166	An alternate way of defining a transitive class. Definition of [Enderton] p. 71. (Contributed by NM, 29-Aug-1993.)
⊢ (Tr 𝐴 ↔ 𝐴 ⊆ 𝒫 𝐴)
Theorem	treq 4167	Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.)
⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))
Theorem	trel 4168	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 4169	In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.)
⊢ (Tr 𝐴 → ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐷 ∧ 𝐷 ∈ 𝐴) → 𝐵 ∈ 𝐴))
Theorem	trss 4170	An element of a transitive class is a subset of the class. (Contributed by NM, 7-Aug-1994.)
⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
Theorem	trin 4171	The intersection of transitive classes is transitive. (Contributed by NM, 9-May-1994.)
⊢ ((Tr 𝐴 ∧ Tr 𝐵) → Tr (𝐴 ∩ 𝐵))
Theorem	tr0 4172	The empty set is transitive. (Contributed by NM, 16-Sep-1993.)
⊢ Tr ∅
Theorem	trv 4173	The universe is transitive. (Contributed by NM, 14-Sep-2003.)
⊢ Tr V
Theorem	triun 4174*	The indexed union of a class of transitive sets is transitive. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (∀𝑥 ∈ 𝐴 Tr 𝐵 → Tr ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	truni 4175*	The union of a class of transitive sets is transitive. Exercise 5(a) of [Enderton] p. 73. (Contributed by Scott Fenton, 21-Feb-2011.) (Proof shortened by Mario Carneiro, 26-Apr-2014.)
⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∪ 𝐴)
Theorem	trint 4176*	The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. (Contributed by Scott Fenton, 25-Feb-2011.)
⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∩ 𝐴)
Theorem	trintssm 4177*	Any inhabited transitive class includes its intersection. Similar to Exercise 3 in [TakeutiZaring] p. 44 (which mistakenly does not include the inhabitedness hypothesis). (Contributed by Jim Kingdon, 22-Aug-2018.)
⊢ ((Tr 𝐴 ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∩ 𝐴 ⊆ 𝐴)
2.2  IZF Set Theory - add the Axioms of Collection and Separation
2.2.1  Introduce the Axiom of Collection
Axiom	ax-coll 4178*	Axiom of Collection. Axiom 7 of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed). It is similar to bnd 4235 but uses a freeness hypothesis in place of one of the distinct variable conditions. (Contributed by Jim Kingdon, 23-Aug-2018.)
⊢ Ⅎ𝑏𝜑    ⇒   ⊢ (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑)
Theorem	repizf 4179*	Axiom of Replacement. Axiom 7' of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed). In our context this is not an axiom, but a theorem proved from ax-coll 4178. It is identical to zfrep6 4180 except for the choice of a freeness hypothesis rather than a disjoint variable condition between 𝑏 and 𝜑. (Contributed by Jim Kingdon, 23-Aug-2018.)
⊢ Ⅎ𝑏𝜑    ⇒   ⊢ (∀𝑥 ∈ 𝑎 ∃!𝑦𝜑 → ∃𝑏∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑)
Theorem	zfrep6 4180*	A version of the Axiom of Replacement. Normally 𝜑 would have free variables 𝑥 and 𝑦. Axiom 6 of [Kunen] p. 12. The Separation Scheme ax-sep 4181 cannot be derived from this version and must be stated as a separate axiom in an axiom system (such as Kunen's) that uses this version. (Contributed by NM, 10-Oct-2003.)
⊢ (∀𝑥 ∈ 𝑧 ∃!𝑦𝜑 → ∃𝑤∀𝑥 ∈ 𝑧 ∃𝑦 ∈ 𝑤 𝜑)
2.2.2  Introduce the Axiom of Separation
Axiom	ax-sep 4181*	The Axiom of Separation of IZF set theory. Axiom 6 of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed, and with a Ⅎ𝑦𝜑 condition replaced by a disjoint variable condition between 𝑦 and 𝜑). The Separation Scheme is a weak form of Frege's Axiom of Comprehension, conditioning it (with 𝑥 ∈ 𝑧) so that it asserts the existence of a collection only if it is smaller than some other collection 𝑧 that already exists. This prevents Russell's paradox ru 3007. In some texts, this scheme is called "Aussonderung" or the Subset Axiom. (Contributed by NM, 11-Sep-2006.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axsep2 4182*	A less restrictive version of the Separation Scheme ax-sep 4181, where variables 𝑥 and 𝑧 can both appear free in the wff 𝜑, which can therefore be thought of as 𝜑(𝑥, 𝑧). This version was derived from the more restrictive ax-sep 4181 with no additional set theory axioms. (Contributed by NM, 10-Dec-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	zfauscl 4183*	Separation Scheme (Aussonderung) using a class variable. To derive this from ax-sep 4181, we invoke the Axiom of Extensionality (indirectly via vtocl 2835), which is needed for the justification of class variable notation. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	bm1.3ii 4184*	Convert implication to equivalence using the Separation Scheme (Aussonderung) ax-sep 4181. Similar to Theorem 1.3ii of [BellMachover] p. 463. (Contributed by NM, 5-Aug-1993.)
⊢ ∃𝑥∀𝑦(𝜑 → 𝑦 ∈ 𝑥)    ⇒   ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑)
Theorem	a9evsep 4185*	Derive a weakened version of ax-i9 1556, where 𝑥 and 𝑦 must be distinct, from Separation ax-sep 4181 and Extensionality ax-ext 2191. The theorem ¬ ∀𝑥¬ 𝑥 = 𝑦 also holds (ax9vsep 4186), but in intuitionistic logic ∃𝑥𝑥 = 𝑦 is stronger. (Contributed by Jim Kingdon, 25-Aug-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑥 𝑥 = 𝑦
Theorem	ax9vsep 4186*	Derive a weakened version of ax-9 1557, where 𝑥 and 𝑦 must be distinct, from Separation ax-sep 4181 and Extensionality ax-ext 2191. In intuitionistic logic a9evsep 4185 is stronger and also holds. (Contributed by NM, 12-Nov-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦
2.2.3  Derive the Null Set Axiom
Theorem	zfnuleu 4187*	Show the uniqueness of the empty set (using the Axiom of Extensionality via bm1.1 2194 to strengthen the hypothesis in the form of axnul 4188). (Contributed by NM, 22-Dec-2007.)
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥    ⇒   ⊢ ∃!𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
Theorem	axnul 4188*	The Null Set Axiom of ZF set theory: there exists a set with no elements. Axiom of Empty Set of [Enderton] p. 18. In some textbooks, this is presented as a separate axiom; here we show it can be derived from Separation ax-sep 4181. This version of the Null Set Axiom tells us that at least one empty set exists, but does not tell us that it is unique - we need the Axiom of Extensionality to do that (see zfnuleu 4187). This theorem should not be referenced by any proof. Instead, use ax-nul 4189 below so that the uses of the Null Set Axiom can be more easily identified. (Contributed by Jeff Hoffman, 3-Feb-2008.) (Revised by NM, 4-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
Axiom	ax-nul 4189*	The Null Set Axiom of IZF set theory. It was derived as axnul 4188 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily. Axiom 4 of [Crosilla] p. "Axioms of CZF and IZF". (Contributed by NM, 7-Aug-2003.)
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
Theorem	0ex 4190	The Null Set Axiom of ZF set theory: the empty set exists. Corollary 5.16 of [TakeutiZaring] p. 20. For the unabbreviated version, see ax-nul 4189. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ ∅ ∈ V
Theorem	csbexga 4191	The existence of proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 𝐵 ∈ 𝑊) → ⦋𝐴 / 𝑥⦌𝐵 ∈ V)
Theorem	csbexa 4192	The existence of proper substitution into a class. (Contributed by NM, 7-Aug-2007.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝐵 ∈ V
2.2.4  Theorems requiring subset and intersection existence
Theorem	nalset 4193*	No set contains all sets. Theorem 41 of [Suppes] p. 30. (Contributed by NM, 23-Aug-1993.)
⊢ ¬ ∃𝑥∀𝑦 𝑦 ∈ 𝑥
Theorem	vnex 4194	The universal class does not exist as a set. (Contributed by NM, 4-Jul-2005.)
⊢ ¬ ∃𝑥 𝑥 = V
Theorem	vprc 4195	The universal class is not a member of itself (and thus is not a set). Proposition 5.21 of [TakeutiZaring] p. 21; our proof, however, does not depend on the Axiom of Regularity. (Contributed by NM, 23-Aug-1993.)
⊢ ¬ V ∈ V
Theorem	nvel 4196	The universal class does not belong to any class. (Contributed by FL, 31-Dec-2006.)
⊢ ¬ V ∈ 𝐴
Theorem	inex1 4197	Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∩ 𝐵) ∈ V
Theorem	inex2 4198	Separation Scheme (Aussonderung) using class notation. (Contributed by NM, 27-Apr-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ∩ 𝐴) ∈ V
Theorem	inex1g 4199	Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)
Theorem	ssex 4200	The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22. This is one way to express the Axiom of Separation ax-sep 4181 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)