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