P. 33 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 3201-3300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cbvreucsf 3201	A more general version of cbvreuv 2838 that has no distinct variable restrictions. Changes bound variables using implicit substitution. (Contributed by Andrew Salmon, 13-Jul-2011.)
⊢ ℲyA    &   ⊢ ℲxB    &   ⊢ Ⅎyφ    &   ⊢ Ⅎxψ    &   ⊢ (x = y → A = B)    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∃!x ∈ A φ ↔ ∃!y ∈ B ψ)
Theorem	cbvrabcsf 3202	A more general version of cbvrab 2858 with no distinct variable restrictions. (Contributed by Andrew Salmon, 13-Jul-2011.)
⊢ ℲyA    &   ⊢ ℲxB    &   ⊢ Ⅎyφ    &   ⊢ Ⅎxψ    &   ⊢ (x = y → A = B)    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ {x ∈ A ∣ φ} = {y ∈ B ∣ ψ}
Theorem	cbvralv2 3203*	Rule used to change the bound variable in a restricted universal quantifier with implicit substitution which also changes the quantifier domain. (Contributed by David Moews, 1-May-2017.)
⊢ (x = y → (ψ ↔ χ))    &   ⊢ (x = y → A = B)    ⇒   ⊢ (∀x ∈ A ψ ↔ ∀y ∈ B χ)
Theorem	cbvrexv2 3204*	Rule used to change the bound variable in a restricted existential quantifier with implicit substitution which also changes the quantifier domain. (Contributed by David Moews, 1-May-2017.)
⊢ (x = y → (ψ ↔ χ))    &   ⊢ (x = y → A = B)    ⇒   ⊢ (∃x ∈ A ψ ↔ ∃y ∈ B χ)
2.1.10  Define boolean set operations
Syntax	cnin 3205	Extend class notation to include anti-intersection (read: "the anti-intersection of A and B").
class (A ⩃ B)
Syntax	ccompl 3206	Extend class notation to include complement. (read: "the complement of A " ).
class ∼ A
Syntax	cdif 3207	Extend class notation to include class difference (read: "A minus B").
class (A ∖ B)
Syntax	cun 3208	Extend class notation to include union of two classes (read: "A union B").
class (A ∪ B)
Syntax	cin 3209	Extend class notation to include the intersection of two classes (read: "A intersect B").
class (A ∩ B)
Syntax	csymdif 3210	Extend class notation to include the symmetric difference of two classes.
class (A ⊕ B)
Theorem	ninjust 3211*	Soundness theorem for df-nin 3212. (Contributed by SF, 10-Jan-2015.)
⊢ {x ∣ (x ∈ A ⊼ x ∈ B)} = {y ∣ (y ∈ A ⊼ y ∈ B)}
Definition	df-nin 3212*	Define the anti-intersection of two classes. This operation is used implicitly after Axiom P1 of [Hailperin] p. 6, though there does not seem to be any notation for it in the literature. (Contributed by SF, 10-Jan-2015.)
⊢ (A ⩃ B) = {x ∣ (x ∈ A ⊼ x ∈ B)}
Definition	df-compl 3213	Define the complement of a class. Compare nic-dfneg 1435. (Contributed by SF, 10-Jan-2015.)
⊢ ∼ A = (A ⩃ A)
Definition	df-in 3214	Define the intersection of two classes. See elin 3220 for membership. (Contributed by SF, 10-Jan-2015.)
⊢ (A ∩ B) = ∼ (A ⩃ B)
Definition	df-un 3215	Define the union of two classes. See elun 3221 for membership. (Contributed by SF, 10-Jan-2015.)
⊢ (A ∪ B) = ( ∼ A ⩃ ∼ B)
Definition	df-dif 3216	Define the difference of two classes. See eldif 3222 for membership. (Contributed by SF, 10-Jan-2015.)
⊢ (A ∖ B) = (A ∩ ∼ B)
Definition	df-symdif 3217	Define the symmetric difference of two classes. Definition IX.9.10, [Rosser] p. 238. (Contributed by SF, 10-Jan-2015.)
⊢ (A ⊕ B) = ((A ∖ B) ∪ (B ∖ A))
Theorem	elning 3218	Membership in anti-intersection. (Contributed by SF, 10-Jan-2015.)
⊢ (A ∈ V → (A ∈ (B ⩃ C) ↔ (A ∈ B ⊼ A ∈ C)))
Theorem	elcomplg 3219	Membership in class complement. (Contributed by SF, 10-Jan-2015.)
⊢ (A ∈ V → (A ∈ ∼ B ↔ ¬ A ∈ B))
Theorem	elin 3220	Membership in intersection. (Contributed by SF, 10-Jan-2015.)
⊢ (A ∈ (B ∩ C) ↔ (A ∈ B ∧ A ∈ C))
Theorem	elun 3221	Membership in union. (Contributed by SF, 10-Jan-2015.)
⊢ (A ∈ (B ∪ C) ↔ (A ∈ B ∨ A ∈ C))
Theorem	eldif 3222	Membership in difference. (Contributed by SF, 10-Jan-2015.)
⊢ (A ∈ (B ∖ C) ↔ (A ∈ B ∧ ¬ A ∈ C))
Theorem	dfdif2 3223*	Alternate definition of class difference. (Contributed by NM, 25-Mar-2004.)
⊢ (A ∖ B) = {x ∈ A ∣ ¬ x ∈ B}
Theorem	elsymdif 3224	Membership in symmetric difference. (Contributed by SF, 10-Jan-2015.)
⊢ (A ∈ (B ⊕ C) ↔ ¬ (A ∈ B ↔ A ∈ C))
Theorem	elnin 3225	Membership in anti-intersection. (Contributed by SF, 10-Jan-2015.)
⊢ A ∈ V    ⇒   ⊢ (A ∈ (B ⩃ C) ↔ (A ∈ B ⊼ A ∈ C))
Theorem	elcompl 3226	Membership in complement. (Contributed by SF, 10-Jan-2015.)
⊢ A ∈ V    ⇒   ⊢ (A ∈ ∼ B ↔ ¬ A ∈ B)
Theorem	nincom 3227	Anti-intersection commutes. (Contributed by SF, 10-Jan-2015.)
⊢ (A ⩃ B) = (B ⩃ A)
Theorem	dblcompl 3228	Double complement law. (Contributed by SF, 10-Jan-2015.)
⊢ ∼ ∼ A = A
Theorem	nfnin 3229	Hypothesis builder for anti-intersection. (Contributed by SF, 2-Jan-2018.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx(A ⩃ B)
Theorem	nfcompl 3230	Hypothesis builder for complement. (Contributed by SF, 2-Jan-2018.)
⊢ ℲxA    ⇒   ⊢ Ⅎx ∼ A
Theorem	nfin 3231	Hypothesis builder for intersection. (Contributed by SF, 2-Jan-2018.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx(A ∩ B)
Theorem	nfun 3232	Hypothesis builder for union. (Contributed by SF, 2-Jan-2018.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx(A ∪ B)
Theorem	nfdif 3233	Hypothesis builder for difference. (Contributed by SF, 2-Jan-2018.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx(A ∖ B)
Theorem	nfsymdif 3234	Hypothesis builder for symmetric difference. (Contributed by SF, 2-Jan-2018.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx(A ⊕ B)
Theorem	nineq1 3235	Equality law for anti-intersection. (Contributed by SF, 11-Jan-2015.)
⊢ (A = B → (A ⩃ C) = (B ⩃ C))
Theorem	nineq2 3236	Equality law for anti-intersection. (Contributed by SF, 11-Jan-2015.)
⊢ (A = B → (C ⩃ A) = (C ⩃ B))
Theorem	nineq12 3237	Equality law for anti-intersection. (Contributed by SF, 11-Jan-2015.)
⊢ ((A = B ∧ C = D) → (A ⩃ C) = (B ⩃ D))
Theorem	nineq1i 3238	Equality inference for anti-intersection. (Contributed by SF, 11-Jan-2015.)
⊢ A = B    ⇒   ⊢ (A ⩃ C) = (B ⩃ C)
Theorem	nineq2i 3239	Equality inference for anti-intersection. (Contributed by SF, 11-Jan-2015.)
⊢ A = B    ⇒   ⊢ (C ⩃ A) = (C ⩃ B)
Theorem	nineq12i 3240	Equality inference for anti-intersection. (Contributed by SF, 11-Jan-2015.)
⊢ A = B    &   ⊢ C = D    ⇒   ⊢ (A ⩃ C) = (B ⩃ D)
Theorem	nineq1d 3241	Equality deduction for anti-intersection. (Contributed by SF, 11-Jan-2015.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A ⩃ C) = (B ⩃ C))
Theorem	nineq2d 3242	Equality deduction for anti-intersection. (Contributed by SF, 11-Jan-2015.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (C ⩃ A) = (C ⩃ B))
Theorem	nineq12d 3243	Equality inference for anti-intersection. (Contributed by SF, 11-Jan-2015.)
⊢ (φ → A = B)    &   ⊢ (φ → C = D)    ⇒   ⊢ (φ → (A ⩃ C) = (B ⩃ D))
Theorem	compleq 3244	Equality law for complement. (Contributed by SF, 11-Jan-2015.)
⊢ (A = B → ∼ A = ∼ B)
Theorem	compleqi 3245	Equality inference for complement. (Contributed by SF, 11-Jan-2015.)
⊢ A = B    ⇒   ⊢ ∼ A = ∼ B
Theorem	compleqd 3246	Equality deduction for complement. (Contributed by SF, 11-Jan-2015.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → ∼ A = ∼ B)
Theorem	difeq1 3247	Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (A = B → (A ∖ C) = (B ∖ C))
Theorem	difeq2 3248	Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (A = B → (C ∖ A) = (C ∖ B))
Theorem	symdifeq1 3249	Equality law for intersection. (Contributed by SF, 11-Jan-2015.)
⊢ (A = B → (A ⊕ C) = (B ⊕ C))
Theorem	symdifeq2 3250	Equality law for intersection. (Contributed by SF, 11-Jan-2015.)
⊢ (A = B → (C ⊕ A) = (C ⊕ B))
Theorem	symdifeq12 3251	Equality law for intersection. (Contributed by SF, 11-Jan-2015.)
⊢ ((A = B ∧ C = D) → (A ⊕ C) = (B ⊕ D))
Theorem	symdifeq1i 3252	Equality inference for symmetric difference. (Contributed by SF, 11-Jan-2015.)
⊢ A = B    ⇒   ⊢ (A ⊕ C) = (B ⊕ C)
Theorem	symdifeq2i 3253	Equality inference for symmetric difference. (Contributed by SF, 11-Jan-2015.)
⊢ A = B    ⇒   ⊢ (C ⊕ A) = (C ⊕ B)
Theorem	symdifeq12i 3254	Equality inference for symmetric difference. (Contributed by SF, 11-Jan-2015.)
⊢ A = B    &   ⊢ C = D    ⇒   ⊢ (A ⊕ C) = (B ⊕ D)
Theorem	symdifeq1d 3255	Equality deduction for symmetric difference. (Contributed by SF, 11-Jan-2015.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A ⊕ C) = (B ⊕ C))
Theorem	symdifeq2d 3256	Equality deduction for symmetric difference. (Contributed by SF, 11-Jan-2015.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (C ⊕ A) = (C ⊕ B))
Theorem	symdifeq12d 3257	Equality inference for symmetric difference. (Contributed by SF, 11-Jan-2015.)
⊢ (φ → A = B)    &   ⊢ (φ → C = D)    ⇒   ⊢ (φ → (A ⊕ C) = (B ⊕ D))
2.1.11  Subclasses and subsets
Syntax	wss 3258	Extend wff notation to include the subclass relation. This is read "A is a subclass of B " or "B includes A." When A exists as a set, it is also read "A is a subset of B."
wff A ⊆ B
Syntax	wpss 3259	Extend wff notation with proper subclass relation.
wff A ⊊ B
Definition	df-ss 3260	Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, { 1 , 2 } ⊆ { 1 , 2 , 3 } (ex-ss in set.mm). Note that A ⊆ A (proved in ssid 3291). Contrast this relationship with the relationship A ⊊ B (as will be defined in df-pss 3262). For a more traditional definition, but requiring a dummy variable, see dfss2 3263. Other possible definitions are given by dfss3 3264, dfss4 3490, sspss 3369, ssequn1 3434, ssequn2 3437, sseqin2 3475, and ssdif0 3610. (Contributed by NM, 27-Apr-1994.)
⊢ (A ⊆ B ↔ (A ∩ B) = A)
Theorem	dfss 3261	Variant of subclass definition df-ss 3260. (Contributed by NM, 3-Sep-2004.)
⊢ (A ⊆ B ↔ A = (A ∩ B))
Definition	df-pss 3262	Define proper subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. For example, { 1 , 2 } ⊊ { 1 , 2 , 3 } (ex-pss in set.mm). Note that ¬ A ⊊ A (proved in pssirr 3370). Contrast this relationship with the relationship A ⊆ B (as defined in df-ss 3260). Other possible definitions are given by dfpss2 3355 and dfpss3 3356. (Contributed by NM, 7-Feb-1996.)
⊢ (A ⊊ B ↔ (A ⊆ B ∧ A ≠ B))
Theorem	dfss2 3263*	Alternate definition of the subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Jan-2002.)
⊢ (A ⊆ B ↔ ∀x(x ∈ A → x ∈ B))
Theorem	dfss3 3264*	Alternate definition of subclass relationship. (Contributed by NM, 14-Oct-1999.)
⊢ (A ⊆ B ↔ ∀x ∈ A x ∈ B)
Theorem	dfss2f 3265	Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 3-Jul-1994.) (Revised by Andrew Salmon, 27-Aug-2011.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ (A ⊆ B ↔ ∀x(x ∈ A → x ∈ B))
Theorem	dfss3f 3266	Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 20-Mar-2004.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ (A ⊆ B ↔ ∀x ∈ A x ∈ B)
Theorem	nfss 3267	If x is not free in A and B, it is not free in A ⊆ B. (Contributed by NM, 27-Dec-1996.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx A ⊆ B
Theorem	ssel 3268	Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.)
⊢ (A ⊆ B → (C ∈ A → C ∈ B))
Theorem	ssel2 3269	Membership relationships follow from a subclass relationship. (Contributed by NM, 7-Jun-2004.)
⊢ ((A ⊆ B ∧ C ∈ A) → C ∈ B)
Theorem	sseli 3270	Membership inference from subclass relationship. (Contributed by NM, 5-Aug-1993.)
⊢ A ⊆ B    ⇒   ⊢ (C ∈ A → C ∈ B)
Theorem	sselii 3271	Membership inference from subclass relationship. (Contributed by NM, 31-May-1999.)
⊢ A ⊆ B    &   ⊢ C ∈ A    ⇒   ⊢ C ∈ B
Theorem	sseldi 3272	Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.)
⊢ A ⊆ B    &   ⊢ (φ → C ∈ A)    ⇒   ⊢ (φ → C ∈ B)
Theorem	sseld 3273	Membership deduction from subclass relationship. (Contributed by NM, 15-Nov-1995.)
⊢ (φ → A ⊆ B)    ⇒   ⊢ (φ → (C ∈ A → C ∈ B))
Theorem	sselda 3274	Membership deduction from subclass relationship. (Contributed by NM, 26-Jun-2014.)
⊢ (φ → A ⊆ B)    ⇒   ⊢ ((φ ∧ C ∈ A) → C ∈ B)
Theorem	sseldd 3275	Membership inference from subclass relationship. (Contributed by NM, 14-Dec-2004.)
⊢ (φ → A ⊆ B)    &   ⊢ (φ → C ∈ A)    ⇒   ⊢ (φ → C ∈ B)
Theorem	ssneld 3276	If a class is not in another class, it is also not in a subclass of that class. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → A ⊆ B)    ⇒   ⊢ (φ → (¬ C ∈ B → ¬ C ∈ A))
Theorem	ssneldd 3277	If an element is not in a class, it is also not in a subclass of that class. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → A ⊆ B)    &   ⊢ (φ → ¬ C ∈ B)    ⇒   ⊢ (φ → ¬ C ∈ A)
Theorem	ssriv 3278*	Inference rule based on subclass definition. (Contributed by NM, 5-Aug-1993.)
⊢ (x ∈ A → x ∈ B)    ⇒   ⊢ A ⊆ B
Theorem	ssrdv 3279*	Deduction rule based on subclass definition. (Contributed by NM, 15-Nov-1995.)
⊢ (φ → (x ∈ A → x ∈ B))    ⇒   ⊢ (φ → A ⊆ B)
Theorem	sstr2 3280	Transitivity of subclasses. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
⊢ (A ⊆ B → (B ⊆ C → A ⊆ C))
Theorem	sstr 3281	Transitivity of subclasses. Theorem 6 of [Suppes] p. 23. (Contributed by NM, 5-Sep-2003.)
⊢ ((A ⊆ B ∧ B ⊆ C) → A ⊆ C)
Theorem	sstri 3282	Subclass transitivity inference. (Contributed by NM, 5-May-2000.)
⊢ A ⊆ B    &   ⊢ B ⊆ C    ⇒   ⊢ A ⊆ C
Theorem	sstrd 3283	Subclass transitivity deduction. (Contributed by NM, 2-Jun-2004.)
⊢ (φ → A ⊆ B)    &   ⊢ (φ → B ⊆ C)    ⇒   ⊢ (φ → A ⊆ C)
Theorem	syl5ss 3284	Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.)
⊢ A ⊆ B    &   ⊢ (φ → B ⊆ C)    ⇒   ⊢ (φ → A ⊆ C)
Theorem	syl6ss 3285	Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (φ → A ⊆ B)    &   ⊢ B ⊆ C    ⇒   ⊢ (φ → A ⊆ C)
Theorem	sylan9ss 3286	A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
⊢ (φ → A ⊆ B)    &   ⊢ (ψ → B ⊆ C)    ⇒   ⊢ ((φ ∧ ψ) → A ⊆ C)
Theorem	sylan9ssr 3287	A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.)
⊢ (φ → A ⊆ B)    &   ⊢ (ψ → B ⊆ C)    ⇒   ⊢ ((ψ ∧ φ) → A ⊆ C)
Theorem	eqss 3288	The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 5-Aug-1993.)
⊢ (A = B ↔ (A ⊆ B ∧ B ⊆ A))
Theorem	eqssi 3289	Infer equality from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 9-Sep-1993.)
⊢ A ⊆ B    &   ⊢ B ⊆ A    ⇒   ⊢ A = B
Theorem	eqssd 3290	Equality deduction from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 27-Jun-2004.)
⊢ (φ → A ⊆ B)    &   ⊢ (φ → B ⊆ A)    ⇒   ⊢ (φ → A = B)
Theorem	ssid 3291	Any class is a subclass of itself. Exercise 10 of [TakeutiZaring] p. 18. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
⊢ A ⊆ A
Theorem	ssv 3292	Any class is a subclass of the universal class. (Contributed by NM, 31-Oct-1995.)
⊢ A ⊆ V
Theorem	sseq1 3293	Equality theorem for subclasses. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
⊢ (A = B → (A ⊆ C ↔ B ⊆ C))
Theorem	sseq2 3294	Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.)
⊢ (A = B → (C ⊆ A ↔ C ⊆ B))
Theorem	sseq12 3295	Equality theorem for the subclass relationship. (Contributed by NM, 31-May-1999.)
⊢ ((A = B ∧ C = D) → (A ⊆ C ↔ B ⊆ D))
Theorem	sseq1i 3296	An equality inference for the subclass relationship. (Contributed by NM, 18-Aug-1993.)
⊢ A = B    ⇒   ⊢ (A ⊆ C ↔ B ⊆ C)
Theorem	sseq2i 3297	An equality inference for the subclass relationship. (Contributed by NM, 30-Aug-1993.)
⊢ A = B    ⇒   ⊢ (C ⊆ A ↔ C ⊆ B)
Theorem	sseq12i 3298	An equality inference for the subclass relationship. (Contributed by NM, 31-May-1999.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
⊢ A = B    &   ⊢ C = D    ⇒   ⊢ (A ⊆ C ↔ B ⊆ D)
Theorem	sseq1d 3299	An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A ⊆ C ↔ B ⊆ C))
Theorem	sseq2d 3300	An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (C ⊆ A ↔ C ⊆ B))