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	nfcrii 2301*	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 2302*	Consequence of the not-free predicate. (Note that unlike nfcr 2300, 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 2303*	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 2304	Equality theorem for class not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- A = B   =>    |- ( F/_ x A <-> F/_ x B )
Theorem	nfcxfr 2305	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 2306	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 2307	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 2308*	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 2309*	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 2310	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x { x | ph }
Theorem	nfnfc1 2311	x is bound in F/_ x A. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x F/_ x A
Theorem	clelsb1f 2312	Substitution for the first argument of the membership predicate in an atomic formula (class version of elsb1 2143). (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 2313	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x ph   =>    |- F/_ x { y | ph }
Theorem	nfaba1 2314	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 14-Oct-2016.)
|- F/_ x { y | A. x ph }
Theorem	nfnfc 2315	Hypothesis builder for F/_ y A. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x A   =>    |- F/ x F/_ y A
Theorem	nfeq 2316	Hypothesis builder for equality. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/ x A = B
Theorem	nfel 2317	Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/ x A e. B
Theorem	nfeq1 2318*	Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x A   =>    |- F/ x A = B
Theorem	nfel1 2319*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x A   =>    |- F/ x A e. B
Theorem	nfeq2 2320*	Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x B   =>    |- F/ x A = B
Theorem	nfel2 2321*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x B   =>    |- F/ x A e. B
Theorem	nfcrd 2322*	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 2323	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 2324	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 2325	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 2326	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 2327*	Bound-variable hypothesis builder for a class abstraction. Version of nfabd 2328 with a disjoint variable condition. (Contributed by Mario Carneiro, 8-Oct-2016.) (Revised by Gino Giotto, 10-Jan-2024.)
|- F/ y ph   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/_ x { y | ps } )
Theorem	nfabd 2328	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 2329	Deduction form of dvelimc 2330. (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 2330	Version of dvelim 2005 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 2331	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 2332	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 2333	Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. See also cleqh 2266. (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 2334	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 2335*	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 2336	Extend wff notation to include inequality.
wff A =/= B
Definition	df-ne 2337	Define inequality. (Contributed by NM, 5-Aug-1993.)
|- ( A =/= B <-> -. A = B )
Theorem	neii 2338	Inference associated with df-ne 2337. (Contributed by BJ, 7-Jul-2018.)
|- A =/= B   =>    |- -. A = B
Theorem	neir 2339	Inference associated with df-ne 2337. (Contributed by BJ, 7-Jul-2018.)
|- -. A = B   =>    |- A =/= B
Theorem	nner 2340	Negation of inequality. (Contributed by Jim Kingdon, 23-Dec-2018.)
|- ( A = B -> -. A =/= B )
Theorem	nnedc 2341	Negation of inequality where equality is decidable. (Contributed by Jim Kingdon, 15-May-2018.)
|- (DECID A = B -> ( -. A =/= B <-> A = B ) )
Theorem	dcned 2342	Decidable equality implies decidable negated equality. (Contributed by Jim Kingdon, 3-May-2020.)
|- ( ph -> DECID A = B )   =>    |- ( ph -> DECID A =/= B )
Theorem	neqned 2343	If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2357. One-way deduction form of df-ne 2337. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2386. (Revised by Wolf Lammen, 22-Nov-2019.)
|- ( ph -> -. A = B )   =>    |- ( ph -> A =/= B )
Theorem	neqne 2344	From non-equality to inequality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( -. A = B -> A =/= B )
Theorem	neirr 2345	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 2346	A contradiction concerning equality implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
|- ( A = B -> ( A =/= B -> ph ) )
Theorem	dcne 2347	Decidable equality expressed in terms of =/=. Basically the same as df-dc 825. (Contributed by Jim Kingdon, 14-Mar-2020.)
|- (DECID A = B <-> ( A = B \/ A =/= B ) )
Theorem	nonconne 2348	Law of noncontradiction with equality and inequality. (Contributed by NM, 3-Feb-2012.)
|- -. ( A = B /\ A =/= B )
Theorem	neeq1 2349	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
|- ( A = B -> ( A =/= C <-> B =/= C ) )
Theorem	neeq2 2350	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
|- ( A = B -> ( C =/= A <-> C =/= B ) )
Theorem	neeq1i 2351	Inference for inequality. (Contributed by NM, 29-Apr-2005.)
|- A = B   =>    |- ( A =/= C <-> B =/= C )
Theorem	neeq2i 2352	Inference for inequality. (Contributed by NM, 29-Apr-2005.)
|- A = B   =>    |- ( C =/= A <-> C =/= B )
Theorem	neeq12i 2353	Inference for inequality. (Contributed by NM, 24-Jul-2012.)
|- A = B   &    |- C = D   =>    |- ( A =/= C <-> B =/= D )
Theorem	neeq1d 2354	Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A =/= C <-> B =/= C ) )
Theorem	neeq2d 2355	Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C =/= A <-> C =/= B ) )
Theorem	neeq12d 2356	Deduction for inequality. (Contributed by NM, 24-Jul-2012.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A =/= C <-> B =/= D ) )
Theorem	neneqd 2357	Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph -> A =/= B )   =>    |- ( ph -> -. A = B )
Theorem	neneq 2358	From inequality to non-equality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A =/= B -> -. A = B )
Theorem	eqnetri 2359	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- A = B   &    |- B =/= C   =>    |- A =/= C
Theorem	eqnetrd 2360	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- ( ph -> A = B )   &    |- ( ph -> B =/= C )   =>    |- ( ph -> A =/= C )
Theorem	eqnetrri 2361	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- A = B   &    |- A =/= C   =>    |- B =/= C
Theorem	eqnetrrd 2362	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- ( ph -> A = B )   &    |- ( ph -> A =/= C )   =>    |- ( ph -> B =/= C )
Theorem	neeqtri 2363	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- A =/= B   &    |- B = C   =>    |- A =/= C
Theorem	neeqtrd 2364	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- ( ph -> A =/= B )   &    |- ( ph -> B = C )   =>    |- ( ph -> A =/= C )
Theorem	neeqtrri 2365	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- A =/= B   &    |- C = B   =>    |- A =/= C
Theorem	neeqtrrd 2366	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- ( ph -> A =/= B )   &    |- ( ph -> C = B )   =>    |- ( ph -> A =/= C )
Theorem	eqnetrrid 2367	B chained equality inference for inequality. (Contributed by NM, 6-Jun-2012.)
|- B = A   &    |- ( ph -> B =/= C )   =>    |- ( ph -> A =/= C )
Theorem	3netr3d 2368	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 2369	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 2370	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 2371	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 2372	Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.)
|- ( A = B <-> ph )   =>    |- ( A =/= B <-> -. ph )
Theorem	necon3bbii 2373	Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.)
|- ( ph <-> A = B )   =>    |- ( -. ph <-> A =/= B )
Theorem	necon3bii 2374	Inference from equality to inequality. (Contributed by NM, 23-Feb-2005.)
|- ( A = B <-> C = D )   =>    |- ( A =/= B <-> C =/= D )
Theorem	necon3abid 2375	Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.)
|- ( ph -> ( A = B <-> ps ) )   =>    |- ( ph -> ( A =/= B <-> -. ps ) )
Theorem	necon3bbid 2376	Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.)
|- ( ph -> ( ps <-> A = B ) )   =>    |- ( ph -> ( -. ps <-> A =/= B ) )
Theorem	necon3bid 2377	Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ph -> ( A = B <-> C = D ) )   =>    |- ( ph -> ( A =/= B <-> C =/= D ) )
Theorem	necon3ad 2378	Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|- ( ph -> ( ps -> A = B ) )   =>    |- ( ph -> ( A =/= B -> -. ps ) )
Theorem	necon3bd 2379	Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|- ( ph -> ( A = B -> ps ) )   =>    |- ( ph -> ( -. ps -> A =/= B ) )
Theorem	necon3d 2380	Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.)
|- ( ph -> ( A = B -> C = D ) )   =>    |- ( ph -> ( C =/= D -> A =/= B ) )
Theorem	nesym 2381	Characterization of inequality in terms of reversed equality (see bicom 139). (Contributed by BJ, 7-Jul-2018.)
|- ( A =/= B <-> -. B = A )
Theorem	nesymi 2382	Inference associated with nesym 2381. (Contributed by BJ, 7-Jul-2018.)
|- A =/= B   =>    |- -. B = A
Theorem	nesymir 2383	Inference associated with nesym 2381. (Contributed by BJ, 7-Jul-2018.)
|- -. A = B   =>    |- B =/= A
Theorem	necon3i 2384	Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.)
|- ( A = B -> C = D )   =>    |- ( C =/= D -> A =/= B )
Theorem	necon3ai 2385	Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|- ( ph -> A = B )   =>    |- ( A =/= B -> -. ph )
Theorem	necon3bi 2386	Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|- ( A = B -> ph )   =>    |- ( -. ph -> A =/= B )
Theorem	necon1aidc 2387	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 15-May-2018.)
|- (DECID ph -> ( -. ph -> A = B ) )   =>    |- (DECID ph -> ( A =/= B -> ph ) )
Theorem	necon1bidc 2388	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 15-May-2018.)
|- (DECID A = B -> ( A =/= B -> ph ) )   =>    |- (DECID A = B -> ( -. ph -> A = B ) )
Theorem	necon1idc 2389	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
|- ( A =/= B -> C = D )   =>    |- (DECID A = B -> ( C =/= D -> A = B ) )
Theorem	necon2ai 2390	Contrapositive inference for inequality. (Contributed by NM, 16-Jan-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
|- ( A = B -> -. ph )   =>    |- ( ph -> A =/= B )
Theorem	necon2bi 2391	Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007.)
|- ( ph -> A =/= B )   =>    |- ( A = B -> -. ph )
Theorem	necon2i 2392	Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.)
|- ( A = B -> C =/= D )   =>    |- ( C = D -> A =/= B )
Theorem	necon2ad 2393	Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
|- ( ph -> ( A = B -> -. ps ) )   =>    |- ( ph -> ( ps -> A =/= B ) )
Theorem	necon2bd 2394	Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
|- ( ph -> ( ps -> A =/= B ) )   =>    |- ( ph -> ( A = B -> -. ps ) )
Theorem	necon2d 2395	Contrapositive inference for inequality. (Contributed by NM, 28-Dec-2008.)
|- ( ph -> ( A = B -> C =/= D ) )   =>    |- ( ph -> ( C = D -> A =/= B ) )
Theorem	necon1abiidc 2396	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
|- (DECID ph -> ( -. ph <-> A = B ) )   =>    |- (DECID ph -> ( A =/= B <-> ph ) )
Theorem	necon1bbiidc 2397	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
|- (DECID A = B -> ( A =/= B <-> ph ) )   =>    |- (DECID A = B -> ( -. ph <-> A = B ) )
Theorem	necon1abiddc 2398	Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
|- ( ph -> (DECID ps -> ( -. ps <-> A = B ) ) )   =>    |- ( ph -> (DECID ps -> ( A =/= B <-> ps ) ) )
Theorem	necon1bbiddc 2399	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
|- ( ph -> (DECID A = B -> ( A =/= B <-> ps ) ) )   =>    |- ( ph -> (DECID A = B -> ( -. ps <-> A = B ) ) )
Theorem	necon2abiidc 2400	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
|- (DECID ph -> ( A = B <-> -. ph ) )   =>    |- (DECID ph -> ( ph <-> A =/= B ) )