P. 34 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 3301-3400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	eqsstri 3301	Substitution of equality into a subclass relationship. (Contributed by NM, 16-Jul-1995.)
⊢ A = B    &   ⊢ B ⊆ C    ⇒   ⊢ A ⊆ C
Theorem	eqsstr3i 3302	Substitution of equality into a subclass relationship. (Contributed by NM, 19-Oct-1999.)
⊢ B = A    &   ⊢ B ⊆ C    ⇒   ⊢ A ⊆ C
Theorem	sseqtri 3303	Substitution of equality into a subclass relationship. (Contributed by NM, 28-Jul-1995.)
⊢ A ⊆ B    &   ⊢ B = C    ⇒   ⊢ A ⊆ C
Theorem	sseqtr4i 3304	Substitution of equality into a subclass relationship. (Contributed by NM, 4-Apr-1995.)
⊢ A ⊆ B    &   ⊢ C = B    ⇒   ⊢ A ⊆ C
Theorem	eqsstrd 3305	Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
⊢ (φ → A = B)    &   ⊢ (φ → B ⊆ C)    ⇒   ⊢ (φ → A ⊆ C)
Theorem	eqsstr3d 3306	Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
⊢ (φ → B = A)    &   ⊢ (φ → B ⊆ C)    ⇒   ⊢ (φ → A ⊆ C)
Theorem	sseqtrd 3307	Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
⊢ (φ → A ⊆ B)    &   ⊢ (φ → B = C)    ⇒   ⊢ (φ → A ⊆ C)
Theorem	sseqtr4d 3308	Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
⊢ (φ → A ⊆ B)    &   ⊢ (φ → C = B)    ⇒   ⊢ (φ → A ⊆ C)
Theorem	3sstr3i 3309	Substitution of equality in both sides of a subclass relationship. (Contributed by NM, 13-Jan-1996.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
⊢ A ⊆ B    &   ⊢ A = C    &   ⊢ B = D    ⇒   ⊢ C ⊆ D
Theorem	3sstr4i 3310	Substitution of equality in both sides of a subclass relationship. (Contributed by NM, 13-Jan-1996.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
⊢ A ⊆ B    &   ⊢ C = A    &   ⊢ D = B    ⇒   ⊢ C ⊆ D
Theorem	3sstr3g 3311	Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 1-Oct-2000.)
⊢ (φ → A ⊆ B)    &   ⊢ A = C    &   ⊢ B = D    ⇒   ⊢ (φ → C ⊆ D)
Theorem	3sstr4g 3312	Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
⊢ (φ → A ⊆ B)    &   ⊢ C = A    &   ⊢ D = B    ⇒   ⊢ (φ → C ⊆ D)
Theorem	3sstr3d 3313	Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 1-Oct-2000.)
⊢ (φ → A ⊆ B)    &   ⊢ (φ → A = C)    &   ⊢ (φ → B = D)    ⇒   ⊢ (φ → C ⊆ D)
Theorem	3sstr4d 3314	Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 30-Nov-1995.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
⊢ (φ → A ⊆ B)    &   ⊢ (φ → C = A)    &   ⊢ (φ → D = B)    ⇒   ⊢ (φ → C ⊆ D)
Theorem	syl5eqss 3315	B chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
⊢ A = B    &   ⊢ (φ → B ⊆ C)    ⇒   ⊢ (φ → A ⊆ C)
Theorem	syl5eqssr 3316	B chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
⊢ B = A    &   ⊢ (φ → B ⊆ C)    ⇒   ⊢ (φ → A ⊆ C)
Theorem	syl6sseq 3317	A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
⊢ (φ → A ⊆ B)    &   ⊢ B = C    ⇒   ⊢ (φ → A ⊆ C)
Theorem	syl6sseqr 3318	A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
⊢ (φ → A ⊆ B)    &   ⊢ C = B    ⇒   ⊢ (φ → A ⊆ C)
Theorem	syl5sseq 3319	Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ B ⊆ A    &   ⊢ (φ → A = C)    ⇒   ⊢ (φ → B ⊆ C)
Theorem	syl5sseqr 3320	Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ B ⊆ A    &   ⊢ (φ → C = A)    ⇒   ⊢ (φ → B ⊆ C)
Theorem	syl6eqss 3321	A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (φ → A = B)    &   ⊢ B ⊆ C    ⇒   ⊢ (φ → A ⊆ C)
Theorem	syl6eqssr 3322	A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (φ → B = A)    &   ⊢ B ⊆ C    ⇒   ⊢ (φ → A ⊆ C)
Theorem	eqimss 3323	Equality implies the subclass relation. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
⊢ (A = B → A ⊆ B)
Theorem	eqimss2 3324	Equality implies the subclass relation. (Contributed by NM, 23-Nov-2003.)
⊢ (B = A → A ⊆ B)
Theorem	eqimssi 3325	Infer subclass relationship from equality. (Contributed by NM, 6-Jan-2007.)
⊢ A = B    ⇒   ⊢ A ⊆ B
Theorem	eqimss2i 3326	Infer subclass relationship from equality. (Contributed by NM, 7-Jan-2007.)
⊢ A = B    ⇒   ⊢ B ⊆ A
Theorem	nssne1 3327	Two classes are different if they don't include the same class. (Contributed by NM, 23-Apr-2015.)
⊢ ((A ⊆ B ∧ ¬ A ⊆ C) → B ≠ C)
Theorem	nssne2 3328	Two classes are different if they are not subclasses of the same class. (Contributed by NM, 23-Apr-2015.)
⊢ ((A ⊆ C ∧ ¬ B ⊆ C) → A ≠ B)
Theorem	nss 3329*	Negation of subclass relationship. Exercise 13 of [TakeutiZaring] p. 18. (Contributed by NM, 25-Feb-1996.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
⊢ (¬ A ⊆ B ↔ ∃x(x ∈ A ∧ ¬ x ∈ B))
Theorem	ssralv 3330*	Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006.)
⊢ (A ⊆ B → (∀x ∈ B φ → ∀x ∈ A φ))
Theorem	ssrexv 3331*	Existential quantification restricted to a subclass. (Contributed by NM, 11-Jan-2007.)
⊢ (A ⊆ B → (∃x ∈ A φ → ∃x ∈ B φ))
Theorem	ralss 3332*	Restricted universal quantification on a subset in terms of superset. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (A ⊆ B → (∀x ∈ A φ ↔ ∀x ∈ B (x ∈ A → φ)))
Theorem	rexss 3333*	Restricted existential quantification on a subset in terms of superset. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (A ⊆ B → (∃x ∈ A φ ↔ ∃x ∈ B (x ∈ A ∧ φ)))
Theorem	ss2ab 3334	Class abstractions in a subclass relationship. (Contributed by NM, 3-Jul-1994.)
⊢ ({x ∣ φ} ⊆ {x ∣ ψ} ↔ ∀x(φ → ψ))
Theorem	abss 3335*	Class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006.)
⊢ ({x ∣ φ} ⊆ A ↔ ∀x(φ → x ∈ A))
Theorem	ssab 3336*	Subclass of a class abstraction. (Contributed by NM, 16-Aug-2006.)
⊢ (A ⊆ {x ∣ φ} ↔ ∀x(x ∈ A → φ))
Theorem	ssabral 3337*	The relation for a subclass of a class abstraction is equivalent to restricted quantification. (Contributed by NM, 6-Sep-2006.)
⊢ (A ⊆ {x ∣ φ} ↔ ∀x ∈ A φ)
Theorem	ss2abi 3338	Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.)
⊢ (φ → ψ)    ⇒   ⊢ {x ∣ φ} ⊆ {x ∣ ψ}
Theorem	ss2abdv 3339*	Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.)
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → {x ∣ ψ} ⊆ {x ∣ χ})
Theorem	abssdv 3340*	Deduction of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.)
⊢ (φ → (ψ → x ∈ A))    ⇒   ⊢ (φ → {x ∣ ψ} ⊆ A)
Theorem	abssi 3341*	Inference of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.)
⊢ (φ → x ∈ A)    ⇒   ⊢ {x ∣ φ} ⊆ A
Theorem	ss2rab 3342	Restricted abstraction classes in a subclass relationship. (Contributed by NM, 30-May-1999.)
⊢ ({x ∈ A ∣ φ} ⊆ {x ∈ A ∣ ψ} ↔ ∀x ∈ A (φ → ψ))
Theorem	rabss 3343*	Restricted class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006.)
⊢ ({x ∈ A ∣ φ} ⊆ B ↔ ∀x ∈ A (φ → x ∈ B))
Theorem	ssrab 3344*	Subclass of a restricted class abstraction. (Contributed by NM, 16-Aug-2006.)
⊢ (B ⊆ {x ∈ A ∣ φ} ↔ (B ⊆ A ∧ ∀x ∈ B φ))
Theorem	ssrabdv 3345*	Subclass of a restricted class abstraction (deduction rule). (Contributed by NM, 31-Aug-2006.)
⊢ (φ → B ⊆ A)    &   ⊢ ((φ ∧ x ∈ B) → ψ)    ⇒   ⊢ (φ → B ⊆ {x ∈ A ∣ ψ})
Theorem	rabssdv 3346*	Subclass of a restricted class abstraction (deduction rule). (Contributed by NM, 2-Feb-2015.)
⊢ ((φ ∧ x ∈ A ∧ ψ) → x ∈ B)    ⇒   ⊢ (φ → {x ∈ A ∣ ψ} ⊆ B)
Theorem	ss2rabdv 3347*	Deduction of restricted abstraction subclass from implication. (Contributed by NM, 30-May-2006.)
⊢ ((φ ∧ x ∈ A) → (ψ → χ))    ⇒   ⊢ (φ → {x ∈ A ∣ ψ} ⊆ {x ∈ A ∣ χ})
Theorem	ss2rabi 3348	Inference of restricted abstraction subclass from implication. (Contributed by NM, 14-Oct-1999.)
⊢ (x ∈ A → (φ → ψ))    ⇒   ⊢ {x ∈ A ∣ φ} ⊆ {x ∈ A ∣ ψ}
Theorem	rabss2 3349*	Subclass law for restricted abstraction. (Contributed by NM, 18-Dec-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (A ⊆ B → {x ∈ A ∣ φ} ⊆ {x ∈ B ∣ φ})
Theorem	ssab2 3350*	Subclass relation for the restriction of a class abstraction. (Contributed by NM, 31-Mar-1995.)
⊢ {x ∣ (x ∈ A ∧ φ)} ⊆ A
Theorem	ssrab2 3351*	Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997.)
⊢ {x ∈ A ∣ φ} ⊆ A
Theorem	rabssab 3352	A restricted class is a subclass of the corresponding unrestricted class. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ {x ∈ A ∣ φ} ⊆ {x ∣ φ}
Theorem	uniiunlem 3353*	A subset relationship useful for converting union to indexed union using dfiun2 4001 or dfiun2g 3999 and intersection to indexed intersection using dfiin2 4002. (Contributed by NM, 5-Oct-2006.) (Proof shortened by Mario Carneiro, 26-Sep-2015.)
⊢ (∀x ∈ A B ∈ D → (∀x ∈ A B ∈ C ↔ {y ∣ ∃x ∈ A y = B} ⊆ C))
Theorem	dfpss2 3354	Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.)
⊢ (A ⊊ B ↔ (A ⊆ B ∧ ¬ A = B))
Theorem	dfpss3 3355	Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (A ⊊ B ↔ (A ⊆ B ∧ ¬ B ⊆ A))
Theorem	psseq1 3356	Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.)
⊢ (A = B → (A ⊊ C ↔ B ⊊ C))
Theorem	psseq2 3357	Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.)
⊢ (A = B → (C ⊊ A ↔ C ⊊ B))
Theorem	psseq1i 3358	An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ A = B    ⇒   ⊢ (A ⊊ C ↔ B ⊊ C)
Theorem	psseq2i 3359	An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ A = B    ⇒   ⊢ (C ⊊ A ↔ C ⊊ B)
Theorem	psseq12i 3360	An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ A = B    &   ⊢ C = D    ⇒   ⊢ (A ⊊ C ↔ B ⊊ D)
Theorem	psseq1d 3361	An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A ⊊ C ↔ B ⊊ C))
Theorem	psseq2d 3362	An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (C ⊊ A ↔ C ⊊ B))
Theorem	psseq12d 3363	An equality deduction for the proper subclass relationship. (Contributed by NM, 9-Jun-2004.)
⊢ (φ → A = B)    &   ⊢ (φ → C = D)    ⇒   ⊢ (φ → (A ⊊ C ↔ B ⊊ D))
Theorem	pssss 3364	A proper subclass is a subclass. Theorem 10 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.)
⊢ (A ⊊ B → A ⊆ B)
Theorem	pssne 3365	Two classes in a proper subclass relationship are not equal. (Contributed by NM, 16-Feb-2015.)
⊢ (A ⊊ B → A ≠ B)
Theorem	pssssd 3366	Deduce subclass from proper subclass. (Contributed by NM, 29-Feb-1996.)
⊢ (φ → A ⊊ B)    ⇒   ⊢ (φ → A ⊆ B)
Theorem	pssned 3367	Proper subclasses are unequal. Deduction form of pssne 3365. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → A ⊊ B)    ⇒   ⊢ (φ → A ≠ B)
Theorem	sspss 3368	Subclass in terms of proper subclass. (Contributed by NM, 25-Feb-1996.)
⊢ (A ⊆ B ↔ (A ⊊ B ∨ A = B))
Theorem	pssirr 3369	Proper subclass is irreflexive. Theorem 7 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.)
⊢ ¬ A ⊊ A
Theorem	pssn2lp 3370	Proper subclass has no 2-cycle loops. Compare Theorem 8 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ¬ (A ⊊ B ∧ B ⊊ A)
Theorem	sspsstri 3371	Two ways of stating trichotomy with respect to inclusion. (Contributed by NM, 12-Aug-2004.)
⊢ ((A ⊆ B ∨ B ⊆ A) ↔ (A ⊊ B ∨ A = B ∨ B ⊊ A))
Theorem	ssnpss 3372	Partial trichotomy law for subclasses. (Contributed by NM, 16-May-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (A ⊆ B → ¬ B ⊊ A)
Theorem	psstr 3373	Transitive law for proper subclass. Theorem 9 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.)
⊢ ((A ⊊ B ∧ B ⊊ C) → A ⊊ C)
Theorem	sspsstr 3374	Transitive law for subclass and proper subclass. (Contributed by NM, 3-Apr-1996.)
⊢ ((A ⊆ B ∧ B ⊊ C) → A ⊊ C)
Theorem	psssstr 3375	Transitive law for subclass and proper subclass. (Contributed by NM, 3-Apr-1996.)
⊢ ((A ⊊ B ∧ B ⊆ C) → A ⊊ C)
Theorem	psstrd 3376	Proper subclass inclusion is transitive. Deduction form of psstr 3373. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → A ⊊ B)    &   ⊢ (φ → B ⊊ C)    ⇒   ⊢ (φ → A ⊊ C)
Theorem	sspsstrd 3377	Transitivity involving subclass and proper subclass inclusion. Deduction form of sspsstr 3374. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → A ⊆ B)    &   ⊢ (φ → B ⊊ C)    ⇒   ⊢ (φ → A ⊊ C)
Theorem	psssstrd 3378	Transitivity involving subclass and proper subclass inclusion. Deduction form of psssstr 3375. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → A ⊊ B)    &   ⊢ (φ → B ⊆ C)    ⇒   ⊢ (φ → A ⊊ C)
Theorem	npss 3379	A class is not a proper subclass of another iff it satisfies a one-directional form of eqss 3287. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (¬ A ⊊ B ↔ (A ⊆ B → A = B))
2.1.12  The difference, union, and intersection of two classes
Theorem	difeq12 3380	Equality theorem for class difference. (Contributed by FL, 31-Aug-2009.)
⊢ ((A = B ∧ C = D) → (A ∖ C) = (B ∖ D))
Theorem	difeq1i 3381	Inference adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ A = B    ⇒   ⊢ (A ∖ C) = (B ∖ C)
Theorem	difeq2i 3382	Inference adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ A = B    ⇒   ⊢ (C ∖ A) = (C ∖ B)
Theorem	difeq12i 3383	Equality inference for class difference. (Contributed by NM, 29-Aug-2004.)
⊢ A = B    &   ⊢ C = D    ⇒   ⊢ (A ∖ C) = (B ∖ D)
Theorem	difeq1d 3384	Deduction adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A ∖ C) = (B ∖ C))
Theorem	difeq2d 3385	Deduction adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (C ∖ A) = (C ∖ B))
Theorem	difeq12d 3386	Equality deduction for class difference. (Contributed by FL, 29-May-2014.)
⊢ (φ → A = B)    &   ⊢ (φ → C = D)    ⇒   ⊢ (φ → (A ∖ C) = (B ∖ D))
Theorem	difeqri 3387*	Inference from membership to difference. (Contributed by NM, 17-May-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((x ∈ A ∧ ¬ x ∈ B) ↔ x ∈ C)    ⇒   ⊢ (A ∖ B) = C
Theorem	eldifi 3388	Implication of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
⊢ (A ∈ (B ∖ C) → A ∈ B)
Theorem	eldifn 3389	Implication of membership in a class difference. (Contributed by NM, 3-May-1994.)
⊢ (A ∈ (B ∖ C) → ¬ A ∈ C)
Theorem	elndif 3390	A set does not belong to a class excluding it. (Contributed by NM, 27-Jun-1994.)
⊢ (A ∈ B → ¬ A ∈ (C ∖ B))
Theorem	neldif 3391	Implication of membership in a class difference. (Contributed by NM, 28-Jun-1994.)
⊢ ((A ∈ B ∧ ¬ A ∈ (B ∖ C)) → A ∈ C)
Theorem	difdif 3392	Double class difference. Exercise 11 of [TakeutiZaring] p. 22. (Contributed by NM, 17-May-1998.)
⊢ (A ∖ (B ∖ A)) = A
Theorem	difss 3393	Subclass relationship for class difference. Exercise 14 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.)
⊢ (A ∖ B) ⊆ A
Theorem	difssd 3394	A difference of two classes is contained in the minuend. Deduction form of difss 3393. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → (A ∖ B) ⊆ A)
Theorem	difss2 3395	If a class is contained in a difference, it is contained in the minuend. (Contributed by David Moews, 1-May-2017.)
⊢ (A ⊆ (B ∖ C) → A ⊆ B)
Theorem	difss2d 3396	If a class is contained in a difference, it is contained in the minuend. Deduction form of difss2 3395. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → A ⊆ (B ∖ C))    ⇒   ⊢ (φ → A ⊆ B)
Theorem	ssdifss 3397	Preservation of a subclass relationship by class difference. (Contributed by NM, 15-Feb-2007.)
⊢ (A ⊆ B → (A ∖ C) ⊆ B)
Theorem	ddif 3398	Double complement under universal class. Exercise 4.10(s) of [Mendelson] p. 231. (Contributed by NM, 8-Jan-2002.)
⊢ (V ∖ (V ∖ A)) = A
Theorem	ssconb 3399	Contraposition law for subsets. (Contributed by NM, 22-Mar-1998.)
⊢ ((A ⊆ C ∧ B ⊆ C) → (A ⊆ (C ∖ B) ↔ B ⊆ (C ∖ A)))
Theorem	sscon 3400	Contraposition law for subsets. Exercise 15 of [TakeutiZaring] p. 22. (Contributed by NM, 22-Mar-1998.)
⊢ (A ⊆ B → (C ∖ B) ⊆ (C ∖ A))