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	hblem 2301*	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 2302*	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 2307 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 2303*	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 2304	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 2305	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 2306	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 2307	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 2308*	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 2309	Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 5-Aug-1993.)
|- ( ph <-> ps )   =>    |- { x | ph } = { x | ps }
Theorem	abbid 2310	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 2311*	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 2312*	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 2313*	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 2314*	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 2315	Substitution of variable in class abstraction. (Contributed by Jim Kingdon, 27-Sep-2018.)
|- F/ y ph   =>    |- { x | ph } = { y | [ y / x ] ph }
Theorem	cbvabw 2316*	Version of cbvab 2317 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 2317	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 2318*	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 2319*	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 2320*	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 2321*	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 2322*	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 2323	Extend wff definition to include the not-free predicate for classes.
wff F/_ x A
Theorem	nfcjust 2324*	Justification theorem for df-nfc 2325. (Contributed by Mario Carneiro, 13-Oct-2016.)
|- ( A. y F/ x y e. A <-> A. z F/ x z e. A )
Definition	df-nfc 2325*	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 1472 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 2326*	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 2327*	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 2328*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( F/_ x A -> F/ x y e. A )
Theorem	nfcrii 2329*	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 2330*	Consequence of the not-free predicate. (Note that unlike nfcr 2328, 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 2331*	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 2332	Equality theorem for class not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- A = B   =>    |- ( F/_ x A <-> F/_ x B )
Theorem	nfcxfr 2333	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 2334	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 2335	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 2336*	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 2337*	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 2338	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x { x | ph }
Theorem	nfnfc1 2339	x is bound in F/_ x A. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x F/_ x A
Theorem	clelsb1f 2340	Substitution for the first argument of the membership predicate in an atomic formula (class version of elsb1 2171). (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 2341	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x ph   =>    |- F/_ x { y | ph }
Theorem	nfaba1 2342	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 14-Oct-2016.)
|- F/_ x { y | A. x ph }
Theorem	nfnfc 2343	Hypothesis builder for F/_ y A. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x A   =>    |- F/ x F/_ y A
Theorem	nfeq 2344	Hypothesis builder for equality. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/ x A = B
Theorem	nfel 2345	Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/ x A e. B
Theorem	nfeq1 2346*	Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x A   =>    |- F/ x A = B
Theorem	nfel1 2347*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x A   =>    |- F/ x A e. B
Theorem	nfeq2 2348*	Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x B   =>    |- F/ x A = B
Theorem	nfel2 2349*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x B   =>    |- F/ x A e. B
Theorem	nfcrd 2350*	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 2351	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 2352	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 2353	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 2354	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 2355*	Bound-variable hypothesis builder for a class abstraction. Version of nfabd 2356 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 2356	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 2357	Deduction form of dvelimc 2358. (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 2358	Version of dvelim 2033 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 2359	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 2360	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 2361	Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. See also cleqh 2293. (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 2362	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 2363*	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 2364	Extend wff notation to include inequality.
wff A =/= B
Definition	df-ne 2365	Define inequality. (Contributed by NM, 5-Aug-1993.)
|- ( A =/= B <-> -. A = B )
Theorem	neii 2366	Inference associated with df-ne 2365. (Contributed by BJ, 7-Jul-2018.)
|- A =/= B   =>    |- -. A = B
Theorem	neir 2367	Inference associated with df-ne 2365. (Contributed by BJ, 7-Jul-2018.)
|- -. A = B   =>    |- A =/= B
Theorem	nner 2368	Negation of inequality. (Contributed by Jim Kingdon, 23-Dec-2018.)
|- ( A = B -> -. A =/= B )
Theorem	nnedc 2369	Negation of inequality where equality is decidable. (Contributed by Jim Kingdon, 15-May-2018.)
|- (DECID A = B -> ( -. A =/= B <-> A = B ) )
Theorem	dcned 2370	Decidable equality implies decidable negated equality. (Contributed by Jim Kingdon, 3-May-2020.)
|- ( ph -> DECID A = B )   =>    |- ( ph -> DECID A =/= B )
Theorem	neqned 2371	If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2385. One-way deduction form of df-ne 2365. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2414. (Revised by Wolf Lammen, 22-Nov-2019.)
|- ( ph -> -. A = B )   =>    |- ( ph -> A =/= B )
Theorem	neqne 2372	From non-equality to inequality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( -. A = B -> A =/= B )
Theorem	neirr 2373	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 2374	A contradiction concerning equality implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
|- ( A = B -> ( A =/= B -> ph ) )
Theorem	dcne 2375	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 2376	Law of noncontradiction with equality and inequality. (Contributed by NM, 3-Feb-2012.)
|- -. ( A = B /\ A =/= B )
Theorem	neeq1 2377	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
|- ( A = B -> ( A =/= C <-> B =/= C ) )
Theorem	neeq2 2378	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
|- ( A = B -> ( C =/= A <-> C =/= B ) )
Theorem	neeq1i 2379	Inference for inequality. (Contributed by NM, 29-Apr-2005.)
|- A = B   =>    |- ( A =/= C <-> B =/= C )
Theorem	neeq2i 2380	Inference for inequality. (Contributed by NM, 29-Apr-2005.)
|- A = B   =>    |- ( C =/= A <-> C =/= B )
Theorem	neeq12i 2381	Inference for inequality. (Contributed by NM, 24-Jul-2012.)
|- A = B   &    |- C = D   =>    |- ( A =/= C <-> B =/= D )
Theorem	neeq1d 2382	Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A =/= C <-> B =/= C ) )
Theorem	neeq2d 2383	Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C =/= A <-> C =/= B ) )
Theorem	neeq12d 2384	Deduction for inequality. (Contributed by NM, 24-Jul-2012.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A =/= C <-> B =/= D ) )
Theorem	neneqd 2385	Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph -> A =/= B )   =>    |- ( ph -> -. A = B )
Theorem	neneq 2386	From inequality to non-equality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A =/= B -> -. A = B )
Theorem	eqnetri 2387	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- A = B   &    |- B =/= C   =>    |- A =/= C
Theorem	eqnetrd 2388	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- ( ph -> A = B )   &    |- ( ph -> B =/= C )   =>    |- ( ph -> A =/= C )
Theorem	eqnetrri 2389	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- A = B   &    |- A =/= C   =>    |- B =/= C
Theorem	eqnetrrd 2390	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- ( ph -> A = B )   &    |- ( ph -> A =/= C )   =>    |- ( ph -> B =/= C )
Theorem	neeqtri 2391	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- A =/= B   &    |- B = C   =>    |- A =/= C
Theorem	neeqtrd 2392	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- ( ph -> A =/= B )   &    |- ( ph -> B = C )   =>    |- ( ph -> A =/= C )
Theorem	neeqtrri 2393	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- A =/= B   &    |- C = B   =>    |- A =/= C
Theorem	neeqtrrd 2394	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- ( ph -> A =/= B )   &    |- ( ph -> C = B )   =>    |- ( ph -> A =/= C )
Theorem	eqnetrrid 2395	B chained equality inference for inequality. (Contributed by NM, 6-Jun-2012.)
|- B = A   &    |- ( ph -> B =/= C )   =>    |- ( ph -> A =/= C )
Theorem	3netr3d 2396	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 2397	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 )
Theorem	3netr3g 2398	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
|- ( ph -> A =/= B )   &    |- A = C   &    |- B = D   =>    |- ( ph -> C =/= D )
Theorem	3netr4g 2399	Substitution of equality into both sides of an inequality. (Contributed by NM, 14-Jun-2012.)
|- ( ph -> A =/= B )   &    |- C = A   &    |- D = B   =>    |- ( ph -> C =/= D )
Theorem	necon3abii 2400	Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.)
|- ( A = B <-> ph )   =>    |- ( A =/= B <-> -. ph )