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	eleq1a 2301	A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.)
|- ( A e. B -> ( C = A -> C e. B ) )
Theorem	eqeltri 2302	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A = B   &    |- B e. C   =>    |- A e. C
Theorem	eqeltrri 2303	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A = B   &    |- A e. C   =>    |- B e. C
Theorem	eleqtri 2304	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A e. B   &    |- B = C   =>    |- A e. C
Theorem	eleqtrri 2305	Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
|- A e. B   &    |- C = B   =>    |- A e. C
Theorem	eqeltrd 2306	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 2307	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 2308	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 2309	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 2310	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 2311	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 2312	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 2313	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 2314	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 2315	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	eqeltrid 2316	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- A = B   &    |- ( ph -> B e. C )   =>    |- ( ph -> A e. C )
Theorem	eqeltrrid 2317	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- B = A   &    |- ( ph -> B e. C )   =>    |- ( ph -> A e. C )
Theorem	eleqtrid 2318	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- A e. B   &    |- ( ph -> B = C )   =>    |- ( ph -> A e. C )
Theorem	eleqtrrid 2319	B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- A e. B   &    |- ( ph -> C = B )   =>    |- ( ph -> A e. C )
Theorem	eqeltrdi 2320	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- ( ph -> A = B )   &    |- B e. C   =>    |- ( ph -> A e. C )
Theorem	eqeltrrdi 2321	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- ( ph -> B = A )   &    |- B e. C   =>    |- ( ph -> A e. C )
Theorem	eleqtrdi 2322	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
|- ( ph -> A e. B )   &    |- B = C   =>    |- ( ph -> A e. C )
Theorem	eleqtrrdi 2323	A membership and equality inference. (Contributed by NM, 24-Apr-2005.)
|- ( ph -> A e. B )   &    |- C = B   =>    |- ( ph -> A e. C )
Theorem	eleq2s 2324	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 2325	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 2326	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 2327	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 2328	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 2329*	Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. See also cleqf 2397. (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 2330	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 2331	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 2332*	Lemma for eqsb1 2333. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
|- ( [ y / x ] x = A <-> y = A )
Theorem	eqsb1 2333*	Substitution for the left-hand side in an equality. Class version of equsb3 2002. (Contributed by Rodolfo Medina, 28-Apr-2010.)
|- ( [ y / x ] x = A <-> y = A )
Theorem	clelsb1 2334*	Substitution for the first argument of the membership predicate in an atomic formula (class version of elsb1 2207). (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 2335*	Substitution for the second argument of the membership predicate in an atomic formula (class version of elsb2 2208). (Contributed by Jim Kingdon, 22-Nov-2018.)
|- ( [ y / x ] A e. x <-> A e. y )
Theorem	hbxfreq 2336	A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfrbi 1518 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 2337*	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 2338*	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 2343 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 2339*	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 2340	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 2341	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 2342	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 2343	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 2344*	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 2345	Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 5-Aug-1993.)
|- ( ph <-> ps )   =>    |- { x | ph } = { x | ps }
Theorem	abbid 2346	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 2347*	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 2348*	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 2349*	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 2350*	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 2351	Substitution of variable in class abstraction. (Contributed by Jim Kingdon, 27-Sep-2018.)
|- F/ y ph   =>    |- { x | ph } = { y | [ y / x ] ph }
Theorem	cbvabw 2352*	Version of cbvab 2353 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 2353	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 2354*	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 2355*	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 2356*	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 2357*	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 2358*	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 2359	Extend wff definition to include the not-free predicate for classes.
wff F/_ x A
Theorem	nfcjust 2360*	Justification theorem for df-nfc 2361. (Contributed by Mario Carneiro, 13-Oct-2016.)
|- ( A. y F/ x y e. A <-> A. z F/ x z e. A )
Definition	df-nfc 2361*	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 1507 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 2362*	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 2363*	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 2364*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( F/_ x A -> F/ x y e. A )
Theorem	nfcrii 2365*	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 2366*	Consequence of the not-free predicate. (Note that unlike nfcr 2364, 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 2367*	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 2368	Equality theorem for class not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- A = B   =>    |- ( F/_ x A <-> F/_ x B )
Theorem	nfcxfr 2369	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 2370	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 2371	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 2372*	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 2373*	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 2374	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x { x | ph }
Theorem	nfnfc1 2375	x is bound in F/_ x A. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x F/_ x A
Theorem	clelsb1f 2376	Substitution for the first argument of the membership predicate in an atomic formula (class version of elsb1 2207). (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 2377	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x ph   =>    |- F/_ x { y | ph }
Theorem	nfaba1 2378	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 14-Oct-2016.)
|- F/_ x { y | A. x ph }
Theorem	nfnfc 2379	Hypothesis builder for F/_ y A. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x A   =>    |- F/ x F/_ y A
Theorem	nfeq 2380	Hypothesis builder for equality. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/ x A = B
Theorem	nfel 2381	Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/ x A e. B
Theorem	nfeq1 2382*	Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x A   =>    |- F/ x A = B
Theorem	nfel1 2383*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x A   =>    |- F/ x A e. B
Theorem	nfeq2 2384*	Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x B   =>    |- F/ x A = B
Theorem	nfel2 2385*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x B   =>    |- F/ x A e. B
Theorem	nfcrd 2386*	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 2387	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 2388	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 2389	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 2390	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 2391*	Bound-variable hypothesis builder for a class abstraction. Version of nfabd 2392 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 2392	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 2393	Deduction form of dvelimc 2394. (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 2394	Version of dvelim 2068 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 2395	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 2396	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 2397	Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. See also cleqh 2329. (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 2398	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 2399*	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 2400	Extend wff notation to include inequality.
wff A =/= B