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.)
|- F/_yA   &   |- F/_xB   &   |- F/yph   &   |- F/xps   &   |- (x = y -> A = B)   &   |- (x = y -> (ph <-> ps))   =>   |- (E!x e. A ph <-> E!y e. B ps)
Theorem	cbvrabcsf 3202	A more general version of cbvrab 2858 with no distinct variable restrictions. (Contributed by Andrew Salmon, 13-Jul-2011.)
|- F/_yA   &   |- F/_xB   &   |- F/yph   &   |- F/xps   &   |- (x = y -> A = B)   &   |- (x = y -> (ph <-> ps))   =>   |- {x e. A | ph} = {y e. B | ps}
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 -> (ps <-> ch))   &   |- (x = y -> A = B)   =>   |- (A.x e. A ps <-> A.y e. B ch)
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 -> (ps <-> ch))   &   |- (x = y -> A = B)   =>   |- (E.x e. A ps <-> E.y e. B ch)
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 &ncap 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 u. B)
Syntax	cin 3209	Extend class notation to include the intersection of two classes (read: "A intersect B").
class (A i^i 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 e. A -/\ x e. B)} = {y | (y e. A -/\ y e. 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 &ncap B) = {x | (x e. A -/\ x e. B)}
Definition	df-compl 3213	Define the complement of a class. Compare nic-dfneg 1435. (Contributed by SF, 10-Jan-2015.)
|- ∼ A = (A &ncap A)
Definition	df-in 3214	Define the intersection of two classes. See elin 3220 for membership. (Contributed by SF, 10-Jan-2015.)
|- (A i^i B) = ∼ (A &ncap B)
Definition	df-un 3215	Define the union of two classes. See elun 3221 for membership. (Contributed by SF, 10-Jan-2015.)
|- (A u. B) = ( ∼ A &ncap ∼ 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 i^i ∼ 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) u. (B \ A))
Theorem	elning 3218	Membership in anti-intersection. (Contributed by SF, 10-Jan-2015.)
|- (A e. V -> (A e. (B &ncap C) <-> (A e. B -/\ A e. C)))
Theorem	elcomplg 3219	Membership in class complement. (Contributed by SF, 10-Jan-2015.)
|- (A e. V -> (A e. ∼ B <-> -. A e. B))
Theorem	elin 3220	Membership in intersection. (Contributed by SF, 10-Jan-2015.)
|- (A e. (B i^i C) <-> (A e. B /\ A e. C))
Theorem	elun 3221	Membership in union. (Contributed by SF, 10-Jan-2015.)
|- (A e. (B u. C) <-> (A e. B \/ A e. C))
Theorem	eldif 3222	Membership in difference. (Contributed by SF, 10-Jan-2015.)
|- (A e. (B \ C) <-> (A e. B /\ -. A e. C))
Theorem	dfdif2 3223*	Alternate definition of class difference. (Contributed by NM, 25-Mar-2004.)
|- (A \ B) = {x e. A | -. x e. B}
Theorem	elsymdif 3224	Membership in symmetric difference. (Contributed by SF, 10-Jan-2015.)
|- (A e. (B (+) C) <-> -. (A e. B <-> A e. C))
Theorem	elnin 3225	Membership in anti-intersection. (Contributed by SF, 10-Jan-2015.)
|- A e. _V   =>   |- (A e. (B &ncap C) <-> (A e. B -/\ A e. C))
Theorem	elcompl 3226	Membership in complement. (Contributed by SF, 10-Jan-2015.)
|- A e. _V   =>   |- (A e. ∼ B <-> -. A e. B)
Theorem	nincom 3227	Anti-intersection commutes. (Contributed by SF, 10-Jan-2015.)
|- (A &ncap B) = (B &ncap 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.)
|- F/_xA   &   |- F/_xB   =>   |- F/_x(A &ncap B)
Theorem	nfcompl 3230	Hypothesis builder for complement. (Contributed by SF, 2-Jan-2018.)
|- F/_xA   =>   |- F/_x ∼ A
Theorem	nfin 3231	Hypothesis builder for intersection. (Contributed by SF, 2-Jan-2018.)
|- F/_xA   &   |- F/_xB   =>   |- F/_x(A i^i B)
Theorem	nfun 3232	Hypothesis builder for union. (Contributed by SF, 2-Jan-2018.)
|- F/_xA   &   |- F/_xB   =>   |- F/_x(A u. B)
Theorem	nfdif 3233	Hypothesis builder for difference. (Contributed by SF, 2-Jan-2018.)
|- F/_xA   &   |- F/_xB   =>   |- F/_x(A \ B)
Theorem	nfsymdif 3234	Hypothesis builder for symmetric difference. (Contributed by SF, 2-Jan-2018.)
|- F/_xA   &   |- F/_xB   =>   |- F/_x(A (+) B)
Theorem	nineq1 3235	Equality law for anti-intersection. (Contributed by SF, 11-Jan-2015.)
|- (A = B -> (A &ncap C) = (B &ncap C))
Theorem	nineq2 3236	Equality law for anti-intersection. (Contributed by SF, 11-Jan-2015.)
|- (A = B -> (C &ncap A) = (C &ncap B))
Theorem	nineq12 3237	Equality law for anti-intersection. (Contributed by SF, 11-Jan-2015.)
|- ((A = B /\ C = D) -> (A &ncap C) = (B &ncap D))
Theorem	nineq1i 3238	Equality inference for anti-intersection. (Contributed by SF, 11-Jan-2015.)
|- A = B   =>   |- (A &ncap C) = (B &ncap C)
Theorem	nineq2i 3239	Equality inference for anti-intersection. (Contributed by SF, 11-Jan-2015.)
|- A = B   =>   |- (C &ncap A) = (C &ncap B)
Theorem	nineq12i 3240	Equality inference for anti-intersection. (Contributed by SF, 11-Jan-2015.)
|- A = B   &   |- C = D   =>   |- (A &ncap C) = (B &ncap D)
Theorem	nineq1d 3241	Equality deduction for anti-intersection. (Contributed by SF, 11-Jan-2015.)
|- (ph -> A = B)   =>   |- (ph -> (A &ncap C) = (B &ncap C))
Theorem	nineq2d 3242	Equality deduction for anti-intersection. (Contributed by SF, 11-Jan-2015.)
|- (ph -> A = B)   =>   |- (ph -> (C &ncap A) = (C &ncap B))
Theorem	nineq12d 3243	Equality inference for anti-intersection. (Contributed by SF, 11-Jan-2015.)
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> (A &ncap C) = (B &ncap 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.)
|- (ph -> A = B)   =>   |- (ph -> ∼ 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.)
|- (ph -> A = B)   =>   |- (ph -> (A (+) C) = (B (+) C))
Theorem	symdifeq2d 3256	Equality deduction for symmetric difference. (Contributed by SF, 11-Jan-2015.)
|- (ph -> A = B)   =>   |- (ph -> (C (+) A) = (C (+) B))
Theorem	symdifeq12d 3257	Equality inference for symmetric difference. (Contributed by SF, 11-Jan-2015.)
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> (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 C_ B
Syntax	wpss 3259	Extend wff notation with proper subclass relation.
wff A C. B
Definition	df-ss 3260	Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, { 1 , 2 } C_ { 1 , 2 , 3 } (ex-ss in set.mm). Note that A C_ A (proved in ssid 3291). Contrast this relationship with the relationship A C. 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 C_ B <-> (A i^i B) = A)
Theorem	dfss 3261	Variant of subclass definition df-ss 3260. (Contributed by NM, 3-Sep-2004.)
|- (A C_ B <-> A = (A i^i B))
Definition	df-pss 3262	Define proper subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. For example, { 1 , 2 } C. { 1 , 2 , 3 } (ex-pss in set.mm). Note that -. A C. A (proved in pssirr 3370). Contrast this relationship with the relationship A C_ 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 C. B <-> (A C_ 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 C_ B <-> A.x(x e. A -> x e. B))
Theorem	dfss3 3264*	Alternate definition of subclass relationship. (Contributed by NM, 14-Oct-1999.)
|- (A C_ B <-> A.x e. A x e. 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.)
|- F/_xA   &   |- F/_xB   =>   |- (A C_ B <-> A.x(x e. A -> x e. B))
Theorem	dfss3f 3266	Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 20-Mar-2004.)
|- F/_xA   &   |- F/_xB   =>   |- (A C_ B <-> A.x e. A x e. B)
Theorem	nfss 3267	If x is not free in A and B, it is not free in A C_ B. (Contributed by NM, 27-Dec-1996.)
|- F/_xA   &   |- F/_xB   =>   |- F/x A C_ B
Theorem	ssel 3268	Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.)
|- (A C_ B -> (C e. A -> C e. B))
Theorem	ssel2 3269	Membership relationships follow from a subclass relationship. (Contributed by NM, 7-Jun-2004.)
|- ((A C_ B /\ C e. A) -> C e. B)
Theorem	sseli 3270	Membership inference from subclass relationship. (Contributed by NM, 5-Aug-1993.)
|- A C_ B   =>   |- (C e. A -> C e. B)
Theorem	sselii 3271	Membership inference from subclass relationship. (Contributed by NM, 31-May-1999.)
|- A C_ B   &   |- C e. A   =>   |- C e. B
Theorem	sseldi 3272	Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.)
|- A C_ B   &   |- (ph -> C e. A)   =>   |- (ph -> C e. B)
Theorem	sseld 3273	Membership deduction from subclass relationship. (Contributed by NM, 15-Nov-1995.)
|- (ph -> A C_ B)   =>   |- (ph -> (C e. A -> C e. B))
Theorem	sselda 3274	Membership deduction from subclass relationship. (Contributed by NM, 26-Jun-2014.)
|- (ph -> A C_ B)   =>   |- ((ph /\ C e. A) -> C e. B)
Theorem	sseldd 3275	Membership inference from subclass relationship. (Contributed by NM, 14-Dec-2004.)
|- (ph -> A C_ B)   &   |- (ph -> C e. A)   =>   |- (ph -> C e. 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.)
|- (ph -> A C_ B)   =>   |- (ph -> (-. C e. B -> -. C e. 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.)
|- (ph -> A C_ B)   &   |- (ph -> -. C e. B)   =>   |- (ph -> -. C e. A)
Theorem	ssriv 3278*	Inference rule based on subclass definition. (Contributed by NM, 5-Aug-1993.)
|- (x e. A -> x e. B)   =>   |- A C_ B
Theorem	ssrdv 3279*	Deduction rule based on subclass definition. (Contributed by NM, 15-Nov-1995.)
|- (ph -> (x e. A -> x e. B))   =>   |- (ph -> A C_ 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 C_ B -> (B C_ C -> A C_ C))
Theorem	sstr 3281	Transitivity of subclasses. Theorem 6 of [Suppes] p. 23. (Contributed by NM, 5-Sep-2003.)
|- ((A C_ B /\ B C_ C) -> A C_ C)
Theorem	sstri 3282	Subclass transitivity inference. (Contributed by NM, 5-May-2000.)
|- A C_ B   &   |- B C_ C   =>   |- A C_ C
Theorem	sstrd 3283	Subclass transitivity deduction. (Contributed by NM, 2-Jun-2004.)
|- (ph -> A C_ B)   &   |- (ph -> B C_ C)   =>   |- (ph -> A C_ C)
Theorem	syl5ss 3284	Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.)
|- A C_ B   &   |- (ph -> B C_ C)   =>   |- (ph -> A C_ C)
Theorem	syl6ss 3285	Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- (ph -> A C_ B)   &   |- B C_ C   =>   |- (ph -> A C_ C)
Theorem	sylan9ss 3286	A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
|- (ph -> A C_ B)   &   |- (ps -> B C_ C)   =>   |- ((ph /\ ps) -> A C_ C)
Theorem	sylan9ssr 3287	A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.)
|- (ph -> A C_ B)   &   |- (ps -> B C_ C)   =>   |- ((ps /\ ph) -> A C_ 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 C_ B /\ B C_ A))
Theorem	eqssi 3289	Infer equality from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 9-Sep-1993.)
|- A C_ B   &   |- B C_ 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.)
|- (ph -> A C_ B)   &   |- (ph -> B C_ A)   =>   |- (ph -> 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 C_ A
Theorem	ssv 3292	Any class is a subclass of the universal class. (Contributed by NM, 31-Oct-1995.)
|- A C_ _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_ C <-> B C_ C))
Theorem	sseq2 3294	Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.)
|- (A = B -> (C C_ A <-> C C_ B))
Theorem	sseq12 3295	Equality theorem for the subclass relationship. (Contributed by NM, 31-May-1999.)
|- ((A = B /\ C = D) -> (A C_ C <-> B C_ D))
Theorem	sseq1i 3296	An equality inference for the subclass relationship. (Contributed by NM, 18-Aug-1993.)
|- A = B   =>   |- (A C_ C <-> B C_ C)
Theorem	sseq2i 3297	An equality inference for the subclass relationship. (Contributed by NM, 30-Aug-1993.)
|- A = B   =>   |- (C C_ A <-> C 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_ C <-> B C_ D)
Theorem	sseq1d 3299	An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)
|- (ph -> A = B)   =>   |- (ph -> (A C_ C <-> B C_ C))
Theorem	sseq2d 3300	An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)
|- (ph -> A = B)   =>   |- (ph -> (C C_ A <-> C C_ B))