P. 25 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 2401-2500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	syl6eq 2401	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
|- (ph -> A = B)   &   |- B = C   =>   |- (ph -> A = C)
Theorem	syl6req 2402	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
|- (ph -> A = B)   &   |- B = C   =>   |- (ph -> C = A)
Theorem	syl6eqr 2403	An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
|- (ph -> A = B)   &   |- C = B   =>   |- (ph -> A = C)
Theorem	syl6reqr 2404	An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
|- (ph -> A = B)   &   |- C = B   =>   |- (ph -> C = A)
Theorem	sylan9eq 2405	An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- (ph -> A = B)   &   |- (ps -> B = C)   =>   |- ((ph /\ ps) -> A = C)
Theorem	sylan9req 2406	An equality transitivity deduction. (Contributed by NM, 23-Jun-2007.)
|- (ph -> B = A)   &   |- (ps -> B = C)   =>   |- ((ph /\ ps) -> A = C)
Theorem	sylan9eqr 2407	An equality transitivity deduction. (Contributed by NM, 8-May-1994.)
|- (ph -> A = B)   &   |- (ps -> B = C)   =>   |- ((ps /\ ph) -> A = C)
Theorem	3eqtr3g 2408	A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.)
|- (ph -> A = B)   &   |- A = C   &   |- B = D   =>   |- (ph -> C = D)
Theorem	3eqtr3a 2409	A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.)
|- A = B   &   |- (ph -> A = C)   &   |- (ph -> B = D)   =>   |- (ph -> C = D)
Theorem	3eqtr4g 2410	A chained equality inference, useful for converting to definitions. (Contributed by NM, 5-Aug-1993.)
|- (ph -> A = B)   &   |- C = A   &   |- D = B   =>   |- (ph -> C = D)
Theorem	3eqtr4a 2411	A chained equality inference, useful for converting to definitions. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- A = B   &   |- (ph -> C = A)   &   |- (ph -> D = B)   =>   |- (ph -> C = D)
Theorem	eq2tri 2412	A compound transitive inference for class equality. (Contributed by NM, 22-Jan-2004.)
|- (A = C -> D = F)   &   |- (B = D -> C = G)   =>   |- ((A = C /\ B = F) <-> (B = D /\ A = G))
Theorem	eleq1 2413	Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
|- (A = B -> (A e. C <-> B e. C))
Theorem	eleq2 2414	Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
|- (A = B -> (C e. A <-> C e. B))
Theorem	eleq12 2415	Equality implies equivalence of membership. (Contributed by NM, 31-May-1999.)
|- ((A = B /\ C = D) -> (A e. C <-> B e. D))
Theorem	eleq1i 2416	Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
|- A = B   =>   |- (A e. C <-> B e. C)
Theorem	eleq2i 2417	Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
|- A = B   =>   |- (C e. A <-> C e. B)
Theorem	eleq12i 2418	Inference from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
|- A = B   &   |- C = D   =>   |- (A e. C <-> B e. D)
Theorem	eleq1d 2419	Deduction from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
|- (ph -> A = B)   =>   |- (ph -> (A e. C <-> B e. C))
Theorem	eleq2d 2420	Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.)
|- (ph -> A = B)   =>   |- (ph -> (C e. A <-> C e. B))
Theorem	eleq12d 2421	Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> (A e. C <-> B e. D))
Theorem	eleq1a 2422	A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.)
|- (A e. B -> (C = A -> C e. B))
Theorem	eqeltri 2423	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A = B   &   |- B e. C   =>   |- A e. C
Theorem	eqeltrri 2424	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A = B   &   |- A e. C   =>   |- B e. C
Theorem	eleqtri 2425	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A e. B   &   |- B = C   =>   |- A e. C
Theorem	eleqtrri 2426	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A e. B   &   |- C = B   =>   |- A e. C
Theorem	eqeltrd 2427	Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.)
|- (ph -> A = B)   &   |- (ph -> B e. C)   =>   |- (ph -> A e. C)
Theorem	eqeltrrd 2428	Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
|- (ph -> A = B)   &   |- (ph -> A e. C)   =>   |- (ph -> B e. C)
Theorem	eleqtrd 2429	Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
|- (ph -> A e. B)   &   |- (ph -> B = C)   =>   |- (ph -> A e. C)
Theorem	eleqtrrd 2430	Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
|- (ph -> A e. B)   &   |- (ph -> C = B)   =>   |- (ph -> A e. C)
Theorem	3eltr3i 2431	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- A e. B   &   |- A = C   &   |- B = D   =>   |- C e. D
Theorem	3eltr4i 2432	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- A e. B   &   |- C = A   &   |- D = B   =>   |- C e. D
Theorem	3eltr3d 2433	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- (ph -> A e. B)   &   |- (ph -> A = C)   &   |- (ph -> B = D)   =>   |- (ph -> C e. D)
Theorem	3eltr4d 2434	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- (ph -> A e. B)   &   |- (ph -> C = A)   &   |- (ph -> D = B)   =>   |- (ph -> C e. D)
Theorem	3eltr3g 2435	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- (ph -> A e. B)   &   |- A = C   &   |- B = D   =>   |- (ph -> C e. D)
Theorem	3eltr4g 2436	Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- (ph -> A e. B)   &   |- C = A   &   |- D = B   =>   |- (ph -> C e. D)
Theorem	syl5eqel 2437	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- A = B   &   |- (ph -> B e. C)   =>   |- (ph -> A e. C)
Theorem	syl5eqelr 2438	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- B = A   &   |- (ph -> B e. C)   =>   |- (ph -> A e. C)
Theorem	syl5eleq 2439	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- A e. B   &   |- (ph -> B = C)   =>   |- (ph -> A e. C)
Theorem	syl5eleqr 2440	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- A e. B   &   |- (ph -> C = B)   =>   |- (ph -> A e. C)
Theorem	syl6eqel 2441	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- (ph -> A = B)   &   |- B e. C   =>   |- (ph -> A e. C)
Theorem	syl6eqelr 2442	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- (ph -> B = A)   &   |- B e. C   =>   |- (ph -> A e. C)
Theorem	syl6eleq 2443	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- (ph -> A e. B)   &   |- B = C   =>   |- (ph -> A e. C)
Theorem	syl6eleqr 2444	A membership and equality inference. (Contributed by NM, 24-Apr-2005.)
|- (ph -> A e. B)   &   |- C = B   =>   |- (ph -> A e. C)
Theorem	eleq2s 2445	Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- (A e. B -> ph)   &   |- C = B   =>   |- (A e. C -> ph)
Theorem	eqneltrd 2446	If a class is not an element of another class, an equal class is also not an element. Deduction form. (Contributed by David Moews, 1-May-2017.)
|- (ph -> A = B)   &   |- (ph -> -. B e. C)   =>   |- (ph -> -. A e. C)
Theorem	eqneltrrd 2447	If a class is not an element of another class, an equal class is also not an element. Deduction form. (Contributed by David Moews, 1-May-2017.)
|- (ph -> A = B)   &   |- (ph -> -. A e. C)   =>   |- (ph -> -. B e. C)
Theorem	neleqtrd 2448	If a class is not an element of another class, it is also not an element of an equal class. Deduction form. (Contributed by David Moews, 1-May-2017.)
|- (ph -> -. C e. A)   &   |- (ph -> A = B)   =>   |- (ph -> -. C e. B)
Theorem	neleqtrrd 2449	If a class is not an element of another class, it is also not an element of an equal class. Deduction form. (Contributed by David Moews, 1-May-2017.)
|- (ph -> -. C e. B)   &   |- (ph -> A = B)   =>   |- (ph -> -. C e. A)
Theorem	cleqh 2450*	Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 5-Aug-1993.)
|- (y e. A -> A.x y e. A)   &   |- (y e. B -> A.x y e. B)   =>   |- (A = B <-> A.x(x e. A <-> x e. B))
Theorem	nelneq 2451	A way of showing two classes are not equal. (Contributed by NM, 1-Apr-1997.)
|- ((A e. C /\ -. B e. C) -> -. A = B)
Theorem	nelneq2 2452	A way of showing two classes are not equal. (Contributed by NM, 12-Jan-2002.)
|- ((A e. B /\ -. A e. C) -> -. B = C)
Theorem	eqsb3lem 2453*	Lemma for eqsb3 2454. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
|- ([y / x]x = A <-> y = A)
Theorem	eqsb3 2454*	Substitution applied to an atomic wff (class version of equsb3 2102). (Contributed by Rodolfo Medina, 28-Apr-2010.)
|- ([y / x]x = A <-> y = A)
Theorem	clelsb3 2455*	Substitution applied to an atomic wff (class version of elsb3 2103). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
|- ([y / x]x e. A <-> y e. A)
Theorem	hbxfreq 2456	A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfrbi 1568 for equivalence version. (Contributed by NM, 21-Aug-2007.)
|- A = B   &   |- (y e. B -> A.x y e. B)   =>   |- (y e. A -> A.x y e. A)
Theorem	hblem 2457*	Change the free variable of a hypothesis builder. Lemma for nfcrii 2482. (Contributed by NM, 5-Aug-1993.) (Revised by Andrew Salmon, 11-Jul-2011.)
|- (y e. A -> A.x y e. A)   =>   |- (z e. A -> A.x z e. A)
Theorem	abeq2 2458*	Equality of a class variable and a class abstraction (also called a class builder). Theorem 5.1 of [Quine] p. 34. This theorem shows the relationship between expressions with class abstractions and expressions with class variables. Note that abbi 2463 and its relatives are among those useful for converting theorems with class variables to equivalent theorems with wff variables, by first substituting a class abstraction for each class variable. Class variables can always be eliminated from a theorem to result in an equivalent theorem with wff variables, and vice-versa. The idea is roughly as follows. To convert a theorem with a wff variable ph (that has a free variable x) to a theorem with a class variable A, we substitute x e. A for ph throughout and simplify, where A is a new class variable not already in the wff. An example is the conversion of zfauscl in set.mm to inex1 in set.mm (look at the instance of zfauscl that occurs in the proof of inex1 ). Conversely, to convert a theorem with a class variable A to one with ph, we substitute {x | ph} for A throughout and simplify, where x and ph are new setvar and wff variables not already in the wff. An example is cp in set.mm , which derives a formula containing wff variables from substitution instances of the class variables in its equivalent formulation cplem2 in set.mm. For more information on class variables, see Quine pp. 15-21 and/or Takeuti and Zaring pp. 10-13. (Contributed by NM, 5-Aug-1993.)
|- (A = {x | ph} <-> A.x(x e. A <-> ph))
Theorem	abeq1 2459*	Equality of a class variable and a class abstraction. (Contributed by NM, 20-Aug-1993.)
|- ({x | ph} = A <-> A.x(ph <-> x e. A))
Theorem	abeq2i 2460	Equality of a class variable and a class abstraction (inference rule). (Contributed by NM, 3-Apr-1996.)
|- A = {x | ph}   =>   |- (x e. A <-> ph)
Theorem	abeq1i 2461	Equality of a class variable and a class abstraction (inference rule). (Contributed by NM, 31-Jul-1994.)
|- {x | ph} = A   =>   |- (ph <-> x e. A)
Theorem	abeq2d 2462	Equality of a class variable and a class abstraction (deduction). (Contributed by NM, 16-Nov-1995.)
|- (ph -> A = {x | ps})   =>   |- (ph -> (x e. A <-> ps))
Theorem	abbi 2463	Equivalent wff's correspond to equal class abstractions. (Contributed by NM, 25-Nov-2013.) (Revised by Mario Carneiro, 11-Aug-2016.)
|- (A.x(ph <-> ps) <-> {x | ph} = {x | ps})
Theorem	abbi2i 2464*	Equality of a class variable and a class abstraction (inference rule). (Contributed by NM, 5-Aug-1993.)
|- (x e. A <-> ph)   =>   |- A = {x | ph}
Theorem	abbii 2465	Equivalent wff's yield equal class abstractions (inference rule). (Contributed by NM, 5-Aug-1993.)
|- (ph <-> ps)   =>   |- {x | ph} = {x | ps}
Theorem	abbid 2466	Equivalent wff's yield equal class abstractions (deduction rule). (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/xph   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> {x | ps} = {x | ch})
Theorem	abbidv 2467*	Equivalent wff's yield equal class abstractions (deduction rule). (Contributed by NM, 10-Aug-1993.)
|- (ph -> (ps <-> ch))   =>   |- (ph -> {x | ps} = {x | ch})
Theorem	abbi2dv 2468*	Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.)
|- (ph -> (x e. A <-> ps))   =>   |- (ph -> A = {x | ps})
Theorem	abbi1dv 2469*	Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.)
|- (ph -> (ps <-> x e. A))   =>   |- (ph -> {x | ps} = A)
Theorem	abid2 2470*	A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35. (Contributed by NM, 26-Dec-1993.)
|- {x | x e. A} = A
Theorem	cbvab 2471	Rule used to change bound variables, using implicit substitution. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- F/yph   &   |- F/xps   &   |- (x = y -> (ph <-> ps))   =>   |- {x | ph} = {y | ps}
Theorem	cbvabv 2472*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-May-1999.)
|- (x = y -> (ph <-> ps))   =>   |- {x | ph} = {y | ps}
Theorem	clelab 2473*	Membership of a class variable in a class abstraction. (Contributed by NM, 23-Dec-1993.)
|- (A e. {x | ph} <-> E.x(x = A /\ ph))
Theorem	clabel 2474*	Membership of a class abstraction in another class. (Contributed by NM, 17-Jan-2006.)
|- ({x | ph} e. A <-> E.y(y e. A /\ A.x(x e. y <-> ph)))
Theorem	sbab 2475*	The right-hand side of the second equality is a way of representing proper substitution of y for x into a class variable. (Contributed by NM, 14-Sep-2003.)
|- (x = y -> A = {z | [y / x]z e. A})
2.1.3  Class form not-free predicate
Syntax	wnfc 2476	Extend wff definition to include the not-free predicate for classes.
wff F/_xA
Theorem	nfcjust 2477*	Justification theorem for df-nfc 2478. (Contributed by Mario Carneiro, 13-Oct-2016.)
|- (A.y F/x y e. A <-> A.z F/x z e. A)
Definition	df-nfc 2478*	Define the not-free predicate for classes. This is read "x is not free in A". Not-free means that the value of x cannot affect the value of A, e.g., any occurrence of x in A is effectively bound by a "for all" or something that expands to one (such as "there exists"). It is defined in terms of the not-free predicate df-nf 1545 for wffs; see that definition for more information. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( F/_xA <-> A.y F/x y e. A)
Theorem	nfci 2479*	Deduce that a class A does not have x free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/x y e. A   =>   |- F/_xA
Theorem	nfcii 2480*	Deduce that a class A does not have x free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- (y e. A -> A.x y e. A)   =>   |- F/_xA
Theorem	nfcr 2481*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( F/_xA -> F/x y e. A)
Theorem	nfcrii 2482*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_xA   =>   |- (y e. A -> A.x y e. A)
Theorem	nfcri 2483*	Consequence of the not-free predicate. (Note that unlike nfcr 2481, this does not require y and A to be disjoint.) (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_xA   =>   |- F/x y e. A
Theorem	nfcd 2484*	Deduce that a class A does not have x free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/yph   &   |- (ph -> F/x y e. A)   =>   |- (ph -> F/_xA)
Theorem	nfceqi 2485	Equality theorem for class not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- A = B   =>   |- ( F/_xA <-> F/_xB)
Theorem	nfcxfr 2486	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- A = B   &   |- F/_xB   =>   |- F/_xA
Theorem	nfcxfrd 2487	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- A = B   &   |- (ph -> F/_xB)   =>   |- (ph -> F/_xA)
Theorem	nfceqdf 2488	An equality theorem for effectively not free. (Contributed by Mario Carneiro, 14-Oct-2016.)
|- F/xph   &   |- (ph -> A = B)   =>   |- (ph -> ( F/_xA <-> F/_xB))
Theorem	nfcv 2489*	If x is disjoint from A, then x is not free in A. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_xA
Theorem	nfcvd 2490*	If x is disjoint from A, then x is not free in A. (Contributed by Mario Carneiro, 7-Oct-2016.)
|- (ph -> F/_xA)
Theorem	nfab1 2491	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_x{x | ph}
Theorem	nfnfc1 2492	x is bound in F/_xA. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/x F/_xA
Theorem	nfab 2493	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/xph   =>   |- F/_x{y | ph}
Theorem	nfaba1 2494	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 14-Oct-2016.)
|- F/_x{y | A.xph}
Theorem	nfnfc 2495	Hypothesis builder for F/_yA. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_xA   =>   |- F/x F/_yA
Theorem	nfeq 2496	Hypothesis builder for equality. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_xA   &   |- F/_xB   =>   |- F/x A = B
Theorem	nfel 2497	Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_xA   &   |- F/_xB   =>   |- F/x A e. B
Theorem	nfeq1 2498*	Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_xA   =>   |- F/x A = B
Theorem	nfel1 2499*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_xA   =>   |- F/x A e. B
Theorem	nfeq2 2500*	Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_xB   =>   |- F/x A = B