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	eqsb1lem 2453*	Lemma for eqsb1 2454. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
|- ([y / x]x = A <-> y = A)
Theorem	eqsb1 2454*	Substitution for the left-hand side in an equality. Class version of equsb3 2102. (Contributed by Rodolfo Medina, 28-Apr-2010.)
|- ([y / x]x = A <-> y = A)
Theorem	clelsb1 2455*	Substitution for the first argument of the membership predicate in an atomic formula (class version of elsb1 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	clelsb2 2456*	Substitution for the second argument of the membership predicate in an atomic formula (class version of elsb2 2104). (Contributed by Jim Kingdon, 22-Nov-2018.)
|- ([y / x]A e. x <-> A e. y)
Theorem	hbxfreq 2457	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 2458*	Change the free variable of a hypothesis builder. Lemma for nfcrii 2483. (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 2459*	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 2464 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 2460*	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 2461	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 2462	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 2463	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 2464	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 2465*	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 2466	Equivalent wff's yield equal class abstractions (inference rule). (Contributed by NM, 5-Aug-1993.)
|- (ph <-> ps)   =>   |- {x | ph} = {x | ps}
Theorem	abbid 2467	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 2468*	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 2469*	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 2470*	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 2471*	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 2472	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 2473*	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 2474*	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 2475*	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 2476*	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 2477	Extend wff definition to include the not-free predicate for classes.
wff F/_xA
Theorem	nfcjust 2478*	Justification theorem for df-nfc 2479. (Contributed by Mario Carneiro, 13-Oct-2016.)
|- (A.y F/x y e. A <-> A.z F/x z e. A)
Definition	df-nfc 2479*	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 2480*	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 2481*	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 2482*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( F/_xA -> F/x y e. A)
Theorem	nfcrii 2483*	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 2484*	Consequence of the not-free predicate. (Note that unlike nfcr 2482, 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 2485*	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 2486	Equality theorem for class not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- A = B   =>   |- ( F/_xA <-> F/_xB)
Theorem	nfcxfr 2487	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 2488	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 2489	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 2490*	If x is disjoint from A, then x is not free in A. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_xA
Theorem	nfcvd 2491*	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 2492	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_x{x | ph}
Theorem	nfnfc1 2493	x is bound in F/_xA. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/x F/_xA
Theorem	nfab 2494	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/xph   =>   |- F/_x{y | ph}
Theorem	nfaba1 2495	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 14-Oct-2016.)
|- F/_x{y | A.xph}
Theorem	nfnfc 2496	Hypothesis builder for F/_yA. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_xA   =>   |- F/x F/_yA
Theorem	nfeq 2497	Hypothesis builder for equality. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_xA   &   |- F/_xB   =>   |- F/x A = B
Theorem	nfel 2498	Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_xA   &   |- F/_xB   =>   |- F/x A e. B
Theorem	nfeq1 2499*	Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_xA   =>   |- F/x A = B
Theorem	nfel1 2500*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_xA   =>   |- F/x A e. B