P. 24 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 2301-2400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	clelsb1 2301*	Substitution for the first argument of the membership predicate in an atomic formula (class version of elsb1 2174). (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 2302*	Substitution for the second argument of the membership predicate in an atomic formula (class version of elsb2 2175). (Contributed by Jim Kingdon, 22-Nov-2018.)
|- ( [ y / x ] A e. x <-> A e. y )
Theorem	hbxfreq 2303	A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfrbi 1486 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 2304*	Change the free variable of a hypothesis builder. (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 2305*	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 2310 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. 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 set and wff variables not already in the wff. 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 2306*	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 2307	Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 3-Apr-1996.)
|- A = { x | ph }   =>    |- ( x e. A <-> ph )
Theorem	abeq1i 2308	Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 31-Jul-1994.)
|- { x | ph } = A   =>    |- ( ph <-> x e. A )
Theorem	abeq2d 2309	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 2310	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 2311*	Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 5-Aug-1993.)
|- ( x e. A <-> ph )   =>    |- A = { x | ph }
Theorem	abbii 2312	Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 5-Aug-1993.)
|- ( ph <-> ps )   =>    |- { x | ph } = { x | ps }
Theorem	abbid 2313	Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> { x | ps } = { x | ch } )
Theorem	abbidv 2314*	Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 10-Aug-1993.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> { x | ps } = { x | ch } )
Theorem	abbi2dv 2315*	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 2316*	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 2317*	A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35. (Contributed by NM, 26-Dec-1993.)
|- { x | x e. A } = A
Theorem	sb8ab 2318	Substitution of variable in class abstraction. (Contributed by Jim Kingdon, 27-Sep-2018.)
|- F/ y ph   =>    |- { x | ph } = { y | [ y / x ] ph }
Theorem	cbvabw 2319*	Version of cbvab 2320 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- { x | ph } = { y | ps }
Theorem	cbvab 2320	Rule used to change bound variables, using implicit substitution. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- { x | ph } = { y | ps }
Theorem	cbvabv 2321*	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 2322*	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 2323*	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 2324*	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.2.1  Elementary properties of class abstractions
Theorem	eqabdv 2325*	Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) (Revised by Wolf Lammen, 6-May-2023.)
|- ( ph -> ( x e. A <-> ps ) )   =>    |- ( ph -> A = { x | ps } )
2.1.3  Class form not-free predicate
Syntax	wnfc 2326	Extend wff definition to include the not-free predicate for classes.
wff F/_ x A
Theorem	nfcjust 2327*	Justification theorem for df-nfc 2328. (Contributed by Mario Carneiro, 13-Oct-2016.)
|- ( A. y F/ x y e. A <-> A. z F/ x z e. A )
Definition	df-nfc 2328*	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 quantifier or something that expands to one (such as "there exists at most one"). It is defined in terms of the not-free predicate df-nf 1475 for wffs; see that definition for more information. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( F/_ x A <-> A. y F/ x y e. A )
Theorem	nfci 2329*	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/_ x A
Theorem	nfcii 2330*	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/_ x A
Theorem	nfcr 2331*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( F/_ x A -> F/ x y e. A )
Theorem	nfcrii 2332*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x A   =>    |- ( y e. A -> A. x y e. A )
Theorem	nfcri 2333*	Consequence of the not-free predicate. (Note that unlike nfcr 2331, this does not require y and A to be disjoint.) (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x A   =>    |- F/ x y e. A
Theorem	nfcd 2334*	Deduce that a class A does not have x free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ y ph   &    |- ( ph -> F/ x y e. A )   =>    |- ( ph -> F/_ x A )
Theorem	nfceqi 2335	Equality theorem for class not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- A = B   =>    |- ( F/_ x A <-> F/_ x B )
Theorem	nfcxfr 2336	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- A = B   &    |- F/_ x B   =>    |- F/_ x A
Theorem	nfcxfrd 2337	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- A = B   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/_ x A )
Theorem	nfceqdf 2338	An equality theorem for effectively not free. (Contributed by Mario Carneiro, 14-Oct-2016.)
|- F/ x ph   &    |- ( ph -> A = B )   =>    |- ( ph -> ( F/_ x A <-> F/_ x B ) )
Theorem	nfcv 2339*	If x is disjoint from A, then x is not free in A. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x A
Theorem	nfcvd 2340*	If x is disjoint from A, then x is not free in A. (Contributed by Mario Carneiro, 7-Oct-2016.)
|- ( ph -> F/_ x A )
Theorem	nfab1 2341	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x { x | ph }
Theorem	nfnfc1 2342	x is bound in F/_ x A. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x F/_ x A
Theorem	clelsb1f 2343	Substitution for the first argument of the membership predicate in an atomic formula (class version of elsb1 2174). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (Revised by Thierry Arnoux, 13-Mar-2017.)
|- F/_ x A   =>    |- ( [ y / x ] x e. A <-> y e. A )
Theorem	nfab 2344	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x ph   =>    |- F/_ x { y | ph }
Theorem	nfaba1 2345	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 14-Oct-2016.)
|- F/_ x { y | A. x ph }
Theorem	nfnfc 2346	Hypothesis builder for F/_ y A. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x A   =>    |- F/ x F/_ y A
Theorem	nfeq 2347	Hypothesis builder for equality. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/ x A = B
Theorem	nfel 2348	Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/ x A e. B
Theorem	nfeq1 2349*	Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x A   =>    |- F/ x A = B
Theorem	nfel1 2350*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x A   =>    |- F/ x A e. B
Theorem	nfeq2 2351*	Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x B   =>    |- F/ x A = B
Theorem	nfel2 2352*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x B   =>    |- F/ x A e. B
Theorem	nfcrd 2353*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( ph -> F/_ x A )   =>    |- ( ph -> F/ x y e. A )
Theorem	nfeqd 2354	Hypothesis builder for equality. (Contributed by Mario Carneiro, 7-Oct-2016.)
|- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/ x A = B )
Theorem	nfeld 2355	Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 7-Oct-2016.)
|- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/ x A e. B )
Theorem	drnfc1 2356	Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- ( A. x x = y -> A = B )   =>    |- ( A. x x = y -> ( F/_ x A <-> F/_ y B ) )
Theorem	drnfc2 2357	Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- ( A. x x = y -> A = B )   =>    |- ( A. x x = y -> ( F/_ z A <-> F/_ z B ) )
Theorem	nfabdw 2358*	Bound-variable hypothesis builder for a class abstraction. Version of nfabd 2359 with a disjoint variable condition. (Contributed by Mario Carneiro, 8-Oct-2016.) (Revised by GG, 10-Jan-2024.)
|- F/ y ph   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/_ x { y | ps } )
Theorem	nfabd 2359	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- F/ y ph   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/_ x { y | ps } )
Theorem	dvelimdc 2360	Deduction form of dvelimc 2361. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- F/ x ph   &    |- F/ z ph   &    |- ( ph -> F/_ x A )   &    |- ( ph -> F/_ z B )   &    |- ( ph -> ( z = y -> A = B ) )   =>    |- ( ph -> ( -. A. x x = y -> F/_ x B ) )
Theorem	dvelimc 2361	Version of dvelim 2036 for classes. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- F/_ x A   &    |- F/_ z B   &    |- ( z = y -> A = B )   =>    |- ( -. A. x x = y -> F/_ x B )
Theorem	nfcvf 2362	If x and y are distinct, then x is not free in y. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- ( -. A. x x = y -> F/_ x y )
Theorem	nfcvf2 2363	If x and y are distinct, then y is not free in x. (Contributed by Mario Carneiro, 5-Dec-2016.)
|- ( -. A. x x = y -> F/_ y x )
Theorem	cleqf 2364	Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. See also cleqh 2296. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
Theorem	abid2f 2365	A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35. (Contributed by NM, 5-Sep-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/_ x A   =>    |- { x | x e. A } = A
Theorem	sbabel 2366*	Theorem to move a substitution in and out of a class abstraction. (Contributed by NM, 27-Sep-2003.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/_ x A   =>    |- ( [ y / x ] { z | ph } e. A <-> { z | [ y / x ] ph } e. A )
2.1.4  Negated equality and membership
2.1.4.1  Negated equality
Syntax	wne 2367	Extend wff notation to include inequality.
wff A =/= B
Definition	df-ne 2368	Define inequality. (Contributed by NM, 5-Aug-1993.)
|- ( A =/= B <-> -. A = B )
Theorem	neii 2369	Inference associated with df-ne 2368. (Contributed by BJ, 7-Jul-2018.)
|- A =/= B   =>    |- -. A = B
Theorem	neir 2370	Inference associated with df-ne 2368. (Contributed by BJ, 7-Jul-2018.)
|- -. A = B   =>    |- A =/= B
Theorem	nner 2371	Negation of inequality. (Contributed by Jim Kingdon, 23-Dec-2018.)
|- ( A = B -> -. A =/= B )
Theorem	nnedc 2372	Negation of inequality where equality is decidable. (Contributed by Jim Kingdon, 15-May-2018.)
|- (DECID A = B -> ( -. A =/= B <-> A = B ) )
Theorem	dcned 2373	Decidable equality implies decidable negated equality. (Contributed by Jim Kingdon, 3-May-2020.)
|- ( ph -> DECID A = B )   =>    |- ( ph -> DECID A =/= B )
Theorem	neqned 2374	If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2388. One-way deduction form of df-ne 2368. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2417. (Revised by Wolf Lammen, 22-Nov-2019.)
|- ( ph -> -. A = B )   =>    |- ( ph -> A =/= B )
Theorem	neqne 2375	From non-equality to inequality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( -. A = B -> A =/= B )
Theorem	neirr 2376	No class is unequal to itself. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|- -. A =/= A
Theorem	eqneqall 2377	A contradiction concerning equality implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
|- ( A = B -> ( A =/= B -> ph ) )
Theorem	dcne 2378	Decidable equality expressed in terms of =/=. Basically the same as df-dc 836. (Contributed by Jim Kingdon, 14-Mar-2020.)
|- (DECID A = B <-> ( A = B \/ A =/= B ) )
Theorem	nonconne 2379	Law of noncontradiction with equality and inequality. (Contributed by NM, 3-Feb-2012.)
|- -. ( A = B /\ A =/= B )
Theorem	neeq1 2380	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
|- ( A = B -> ( A =/= C <-> B =/= C ) )
Theorem	neeq2 2381	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
|- ( A = B -> ( C =/= A <-> C =/= B ) )
Theorem	neeq1i 2382	Inference for inequality. (Contributed by NM, 29-Apr-2005.)
|- A = B   =>    |- ( A =/= C <-> B =/= C )
Theorem	neeq2i 2383	Inference for inequality. (Contributed by NM, 29-Apr-2005.)
|- A = B   =>    |- ( C =/= A <-> C =/= B )
Theorem	neeq12i 2384	Inference for inequality. (Contributed by NM, 24-Jul-2012.)
|- A = B   &    |- C = D   =>    |- ( A =/= C <-> B =/= D )
Theorem	neeq1d 2385	Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A =/= C <-> B =/= C ) )
Theorem	neeq2d 2386	Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C =/= A <-> C =/= B ) )
Theorem	neeq12d 2387	Deduction for inequality. (Contributed by NM, 24-Jul-2012.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A =/= C <-> B =/= D ) )
Theorem	neneqd 2388	Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph -> A =/= B )   =>    |- ( ph -> -. A = B )
Theorem	neneq 2389	From inequality to non-equality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A =/= B -> -. A = B )
Theorem	eqnetri 2390	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- A = B   &    |- B =/= C   =>    |- A =/= C
Theorem	eqnetrd 2391	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- ( ph -> A = B )   &    |- ( ph -> B =/= C )   =>    |- ( ph -> A =/= C )
Theorem	eqnetrri 2392	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- A = B   &    |- A =/= C   =>    |- B =/= C
Theorem	eqnetrrd 2393	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- ( ph -> A = B )   &    |- ( ph -> A =/= C )   =>    |- ( ph -> B =/= C )
Theorem	neeqtri 2394	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- A =/= B   &    |- B = C   =>    |- A =/= C
Theorem	neeqtrd 2395	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- ( ph -> A =/= B )   &    |- ( ph -> B = C )   =>    |- ( ph -> A =/= C )
Theorem	neeqtrri 2396	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- A =/= B   &    |- C = B   =>    |- A =/= C
Theorem	neeqtrrd 2397	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- ( ph -> A =/= B )   &    |- ( ph -> C = B )   =>    |- ( ph -> A =/= C )
Theorem	eqnetrrid 2398	B chained equality inference for inequality. (Contributed by NM, 6-Jun-2012.)
|- B = A   &    |- ( ph -> B =/= C )   =>    |- ( ph -> A =/= C )
Theorem	3netr3d 2399	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
|- ( ph -> A =/= B )   &    |- ( ph -> A = C )   &    |- ( ph -> B = D )   =>    |- ( ph -> C =/= D )
Theorem	3netr4d 2400	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
|- ( ph -> A =/= B )   &    |- ( ph -> C = A )   &    |- ( ph -> D = B )   =>    |- ( ph -> C =/= D )