P. 25 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 2401-2500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	necon3bbii 2401	Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.)
|- ( ph <-> A = B )   =>    |- ( -. ph <-> A =/= B )
Theorem	necon3bii 2402	Inference from equality to inequality. (Contributed by NM, 23-Feb-2005.)
|- ( A = B <-> C = D )   =>    |- ( A =/= B <-> C =/= D )
Theorem	necon3abid 2403	Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.)
|- ( ph -> ( A = B <-> ps ) )   =>    |- ( ph -> ( A =/= B <-> -. ps ) )
Theorem	necon3bbid 2404	Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.)
|- ( ph -> ( ps <-> A = B ) )   =>    |- ( ph -> ( -. ps <-> A =/= B ) )
Theorem	necon3bid 2405	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 2406	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 2407	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 2408	Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.)
|- ( ph -> ( A = B -> C = D ) )   =>    |- ( ph -> ( C =/= D -> A =/= B ) )
Theorem	nesym 2409	Characterization of inequality in terms of reversed equality (see bicom 140). (Contributed by BJ, 7-Jul-2018.)
|- ( A =/= B <-> -. B = A )
Theorem	nesymi 2410	Inference associated with nesym 2409. (Contributed by BJ, 7-Jul-2018.)
|- A =/= B   =>    |- -. B = A
Theorem	nesymir 2411	Inference associated with nesym 2409. (Contributed by BJ, 7-Jul-2018.)
|- -. A = B   =>    |- B =/= A
Theorem	necon3i 2412	Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.)
|- ( A = B -> C = D )   =>    |- ( C =/= D -> A =/= B )
Theorem	necon3ai 2413	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 2414	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 2415	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 15-May-2018.)
|- (DECID ph -> ( -. ph -> A = B ) )   =>    |- (DECID ph -> ( A =/= B -> ph ) )
Theorem	necon1bidc 2416	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 2417	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
|- ( A =/= B -> C = D )   =>    |- (DECID A = B -> ( C =/= D -> A = B ) )
Theorem	necon2ai 2418	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 2419	Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007.)
|- ( ph -> A =/= B )   =>    |- ( A = B -> -. ph )
Theorem	necon2i 2420	Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.)
|- ( A = B -> C =/= D )   =>    |- ( C = D -> A =/= B )
Theorem	necon2ad 2421	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 2422	Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
|- ( ph -> ( ps -> A =/= B ) )   =>    |- ( ph -> ( A = B -> -. ps ) )
Theorem	necon2d 2423	Contrapositive inference for inequality. (Contributed by NM, 28-Dec-2008.)
|- ( ph -> ( A = B -> C =/= D ) )   =>    |- ( ph -> ( C = D -> A =/= B ) )
Theorem	necon1abiidc 2424	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
|- (DECID ph -> ( -. ph <-> A = B ) )   =>    |- (DECID ph -> ( A =/= B <-> ph ) )
Theorem	necon1bbiidc 2425	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 2426	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 2427	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 2428	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
|- (DECID ph -> ( A = B <-> -. ph ) )   =>    |- (DECID ph -> ( ph <-> A =/= B ) )
Theorem	necon2bbiidc 2429	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
|- (DECID A = B -> ( ph <-> A =/= B ) )   =>    |- (DECID A = B -> ( A = B <-> -. ph ) )
Theorem	necon2abiddc 2430	Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
|- ( ph -> (DECID ps -> ( A = B <-> -. ps ) ) )   =>    |- ( ph -> (DECID ps -> ( ps <-> A =/= B ) ) )
Theorem	necon2bbiddc 2431	Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
|- ( ph -> (DECID A = B -> ( ps <-> A =/= B ) ) )   =>    |- ( ph -> (DECID A = B -> ( A = B <-> -. ps ) ) )
Theorem	necon4aidc 2432	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
|- (DECID A = B -> ( A =/= B -> -. ph ) )   =>    |- (DECID A = B -> ( ph -> A = B ) )
Theorem	necon4idc 2433	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
|- (DECID A = B -> ( A =/= B -> C =/= D ) )   =>    |- (DECID A = B -> ( C = D -> A = B ) )
Theorem	necon4addc 2434	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 17-May-2018.)
|- ( ph -> (DECID A = B -> ( A =/= B -> -. ps ) ) )   =>    |- ( ph -> (DECID A = B -> ( ps -> A = B ) ) )
Theorem	necon4bddc 2435	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 17-May-2018.)
|- ( ph -> (DECID ps -> ( -. ps -> A =/= B ) ) )   =>    |- ( ph -> (DECID ps -> ( A = B -> ps ) ) )
Theorem	necon4ddc 2436	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 17-May-2018.)
|- ( ph -> (DECID A = B -> ( A =/= B -> C =/= D ) ) )   =>    |- ( ph -> (DECID A = B -> ( C = D -> A = B ) ) )
Theorem	necon4abiddc 2437	Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 18-May-2018.)
|- ( ph -> (DECID A = B -> (DECID ps -> ( A =/= B <-> -. ps ) ) ) )   =>    |- ( ph -> (DECID A = B -> (DECID ps -> ( A = B <-> ps ) ) ) )
Theorem	necon4bbiddc 2438	Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
|- ( ph -> (DECID ps -> (DECID A = B -> ( -. ps <-> A =/= B ) ) ) )   =>    |- ( ph -> (DECID ps -> (DECID A = B -> ( ps <-> A = B ) ) ) )
Theorem	necon4biddc 2439	Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
|- ( ph -> (DECID A = B -> (DECID C = D -> ( A =/= B <-> C =/= D ) ) ) )   =>    |- ( ph -> (DECID A = B -> (DECID C = D -> ( A = B <-> C = D ) ) ) )
Theorem	necon1addc 2440	Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
|- ( ph -> (DECID ps -> ( -. ps -> A = B ) ) )   =>    |- ( ph -> (DECID ps -> ( A =/= B -> ps ) ) )
Theorem	necon1bddc 2441	Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
|- ( ph -> (DECID A = B -> ( A =/= B -> ps ) ) )   =>    |- ( ph -> (DECID A = B -> ( -. ps -> A = B ) ) )
Theorem	necon1ddc 2442	Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
|- ( ph -> (DECID A = B -> ( A =/= B -> C = D ) ) )   =>    |- ( ph -> (DECID A = B -> ( C =/= D -> A = B ) ) )
Theorem	neneqad 2443	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.)
|- ( ph -> -. A = B )   =>    |- ( ph -> A =/= B )
Theorem	nebidc 2444	Contraposition law for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
|- (DECID A = B -> (DECID C = D -> ( ( A = B <-> C = D ) <-> ( A =/= B <-> C =/= D ) ) ) )
Theorem	pm13.18 2445	Theorem *13.18 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
|- ( ( A = B /\ A =/= C ) -> B =/= C )
Theorem	pm13.181 2446	Theorem *13.181 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
|- ( ( A = B /\ B =/= C ) -> A =/= C )
Theorem	pm2.21ddne 2447	A contradiction implies anything. Equality/inequality deduction form. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A = B )   &    |- ( ph -> A =/= B )   =>    |- ( ph -> ps )
Theorem	necom 2448	Commutation of inequality. (Contributed by NM, 14-May-1999.)
|- ( A =/= B <-> B =/= A )
Theorem	necomi 2449	Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.)
|- A =/= B   =>    |- B =/= A
Theorem	necomd 2450	Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)
|- ( ph -> A =/= B )   =>    |- ( ph -> B =/= A )
Theorem	neanior 2451	A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
|- ( ( A =/= B /\ C =/= D ) <-> -. ( A = B \/ C = D ) )
Theorem	ne3anior 2452	A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013.) (Proof rewritten by Jim Kingdon, 19-May-2018.)
|- ( ( A =/= B /\ C =/= D /\ E =/= F ) <-> -. ( A = B \/ C = D \/ E = F ) )
Theorem	nemtbir 2453	An inference from an inequality, related to modus tollens. (Contributed by NM, 13-Apr-2007.)
|- A =/= B   &    |- ( ph <-> A = B )   =>    |- -. ph
Theorem	nelne1 2454	Two classes are different if they don't contain the same element. (Contributed by NM, 3-Feb-2012.)
|- ( ( A e. B /\ -. A e. C ) -> B =/= C )
Theorem	nelne2 2455	Two classes are different if they don't belong to the same class. (Contributed by NM, 25-Jun-2012.)
|- ( ( A e. C /\ -. B e. C ) -> A =/= B )
Theorem	nelelne 2456	Two classes are different if they don't belong to the same class. (Contributed by Rodolfo Medina, 17-Oct-2010.) (Proof shortened by AV, 10-May-2020.)
|- ( -. A e. B -> ( C e. B -> C =/= A ) )
Theorem	nfne 2457	Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/ x A =/= B
Theorem	nfned 2458	Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/ x A =/= B )
2.1.4.2  Negated membership
Syntax	wnel 2459	Extend wff notation to include negated membership.
wff A e/ B
Definition	df-nel 2460	Define negated membership. (Contributed by NM, 7-Aug-1994.)
|- ( A e/ B <-> -. A e. B )
Theorem	neli 2461	Inference associated with df-nel 2460. (Contributed by BJ, 7-Jul-2018.)
|- A e/ B   =>    |- -. A e. B
Theorem	nelir 2462	Inference associated with df-nel 2460. (Contributed by BJ, 7-Jul-2018.)
|- -. A e. B   =>    |- A e/ B
Theorem	neleq1 2463	Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
|- ( A = B -> ( A e/ C <-> B e/ C ) )
Theorem	neleq2 2464	Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
|- ( A = B -> ( C e/ A <-> C e/ B ) )
Theorem	neleq12d 2465	Equality theorem for negated membership. (Contributed by FL, 10-Aug-2016.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A e/ C <-> B e/ D ) )
Theorem	nfnel 2466	Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/ x A e/ B
Theorem	nfneld 2467	Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/ x A e/ B )
Theorem	elnelne1 2468	Two classes are different if they don't contain the same element. (Contributed by AV, 28-Jan-2020.)
|- ( ( A e. B /\ A e/ C ) -> B =/= C )
Theorem	elnelne2 2469	Two classes are different if they don't belong to the same class. (Contributed by AV, 28-Jan-2020.)
|- ( ( A e. C /\ B e/ C ) -> A =/= B )
Theorem	nelcon3d 2470	Contrapositive law deduction for negated membership. (Contributed by AV, 28-Jan-2020.)
|- ( ph -> ( A e. B -> C e. D ) )   =>    |- ( ph -> ( C e/ D -> A e/ B ) )
Theorem	elnelall 2471	A contradiction concerning membership implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
|- ( A e. B -> ( A e/ B -> ph ) )
2.1.5  Restricted quantification
Syntax	wral 2472	Extend wff notation to include restricted universal quantification.
wff A. x e. A ph
Syntax	wrex 2473	Extend wff notation to include restricted existential quantification.
wff E. x e. A ph
Syntax	wreu 2474	Extend wff notation to include restricted existential uniqueness.
wff E! x e. A ph
Syntax	wrmo 2475	Extend wff notation to include restricted "at most one".
wff E* x e. A ph
Syntax	crab 2476	Extend class notation to include the restricted class abstraction (class builder).
class { x e. A | ph }
Definition	df-ral 2477	Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22. (Contributed by NM, 19-Aug-1993.)
|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
Definition	df-rex 2478	Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22. (Contributed by NM, 30-Aug-1993.)
|- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
Definition	df-reu 2479	Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.)
|- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
Definition	df-rmo 2480	Define restricted "at most one". (Contributed by NM, 16-Jun-2017.)
|- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
Definition	df-rab 2481	Define a restricted class abstraction (class builder), which is the class of all x in A such that ph is true. Definition of [TakeutiZaring] p. 20. (Contributed by NM, 22-Nov-1994.)
|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
Theorem	ralnex 2482	Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
|- ( A. x e. A -. ph <-> -. E. x e. A ph )
Theorem	rexnalim 2483	Relationship between restricted universal and existential quantifiers. In classical logic this would be a biconditional. (Contributed by Jim Kingdon, 17-Aug-2018.)
|- ( E. x e. A -. ph -> -. A. x e. A ph )
Theorem	nnral 2484	The double negation of a universal quantification implies the universal quantification of the double negation. Restricted quantifier version of nnal 1660. (Contributed by Jim Kingdon, 1-Aug-2024.)
|- ( -. -. A. x e. A ph -> A. x e. A -. -. ph )
Theorem	dfrex2dc 2485	Relationship between restricted universal and existential quantifiers. (Contributed by Jim Kingdon, 29-Jun-2022.)
|- (DECID E. x e. A ph -> ( E. x e. A ph <-> -. A. x e. A -. ph ) )
Theorem	ralexim 2486	Relationship between restricted universal and existential quantifiers. (Contributed by Jim Kingdon, 17-Aug-2018.)
|- ( A. x e. A ph -> -. E. x e. A -. ph )
Theorem	rexalim 2487	Relationship between restricted universal and existential quantifiers. (Contributed by Jim Kingdon, 17-Aug-2018.)
|- ( E. x e. A ph -> -. A. x e. A -. ph )
Theorem	ralbida 2488	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 6-Oct-2003.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )
Theorem	rexbida 2489	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 6-Oct-2003.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )
Theorem	ralbidva 2490*	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 4-Mar-1997.)
|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )
Theorem	rexbidva 2491*	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 9-Mar-1997.)
|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )
Theorem	ralbid 2492	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 27-Jun-1998.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )
Theorem	rexbid 2493	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 27-Jun-1998.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )
Theorem	ralbidv 2494*	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 20-Nov-1994.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )
Theorem	rexbidv 2495*	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 20-Nov-1994.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )
Theorem	ralbidv2 2496*	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 6-Apr-1997.)
|- ( ph -> ( ( x e. A -> ps ) <-> ( x e. B -> ch ) ) )   =>    |- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) )
Theorem	rexbidv2 2497*	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 22-May-1999.)
|- ( ph -> ( ( x e. A /\ ps ) <-> ( x e. B /\ ch ) ) )   =>    |- ( ph -> ( E. x e. A ps <-> E. x e. B ch ) )
Theorem	ralbid2 2498	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by BJ, 14-Jul-2024.)
|- F/ x ph   &    |- ( ph -> ( ( x e. A -> ps ) <-> ( x e. B -> ch ) ) )   =>    |- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) )
Theorem	rexbid2 2499	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by BJ, 14-Jul-2024.)
|- F/ x ph   &    |- ( ph -> ( ( x e. A /\ ps ) <-> ( x e. B /\ ch ) ) )   =>    |- ( ph -> ( E. x e. A ps <-> E. x e. B ch ) )
Theorem	ralbii 2500	Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.)
|- ( ph <-> ps )   =>    |- ( A. x e. A ph <-> A. x e. A ps )