mmtheorems18 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12229

Statement List for Metamath Proof Explorer - 1701-1800 - Page 18 of 123

Type	Label	Description
Statement
Theorem	dfral2 1701	Relationship between restricted universal and existential quantifiers.
|- (A.x e. A ph <-> -. E.x e. A -. ph)
Theorem	dfrex2 1702	Relationship between restricted universal and existential quantifiers.
|- (E.x e. A ph <-> -. A.x e. A -. ph)
Theorem	ralbida 1703	Formula-building rule for restricted universal quantifier (deduction rule).
|- (ph -> A.xph)   &   |- ((ph /\ x e. A) -> (ps <-> ch))   =>   |- (ph -> (A.x e. A ps <-> A.x e. A ch))
Theorem	rexbida 1704	Formula-building rule for restricted existential quantifier (deduction rule).
|- (ph -> A.xph)   &   |- ((ph /\ x e. A) -> (ps <-> ch))   =>   |- (ph -> (E.x e. A ps <-> E.x e. A ch))
Theorem	ralbidva 1705	Formula-building rule for restricted universal quantifier (deduction rule).
|- ((ph /\ x e. A) -> (ps <-> ch))   =>   |- (ph -> (A.x e. A ps <-> A.x e. A ch))
Theorem	rexbidva 1706	Formula-building rule for restricted existential quantifier (deduction rule).
|- ((ph /\ x e. A) -> (ps <-> ch))   =>   |- (ph -> (E.x e. A ps <-> E.x e. A ch))
Theorem	ralbid 1707	Formula-building rule for restricted universal quantifier (deduction rule).
|- (ph -> A.xph)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> (A.x e. A ps <-> A.x e. A ch))
Theorem	rexbid 1708	Formula-building rule for restricted existential quantifier (deduction rule).
|- (ph -> A.xph)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> (E.x e. A ps <-> E.x e. A ch))
Theorem	ralbidv 1709	Formula-building rule for restricted universal quantifier (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> (A.x e. A ps <-> A.x e. A ch))
Theorem	rexbidv 1710	Formula-building rule for restricted existential quantifier (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> (E.x e. A ps <-> E.x e. A ch))
Theorem	ralbidv2 1711	Formula-building rule for restricted universal quantifier (deduction rule).
|- (ph -> ((x e. A -> ps) <-> (x e. B -> ch)))   =>   |- (ph -> (A.x e. A ps <-> A.x e. B ch))
Theorem	rexbidv2 1712	Formula-building rule for restricted existential quantifier (deduction rule).
|- (ph -> ((x e. A /\ ps) <-> (x e. B /\ ch)))   =>   |- (ph -> (E.x e. A ps <-> E.x e. B ch))
Theorem	ralbii 1713	Inference adding restricted universal quantifier to both sides of an equivalence.
|- (ph <-> ps)   =>   |- (A.x e. A ph <-> A.x e. A ps)
Theorem	rexbii 1714	Inference adding restricted existential quantifier to both sides of an equivalence.
|- (ph <-> ps)   =>   |- (E.x e. A ph <-> E.x e. A ps)
Theorem	2ralbii 1715	Inference adding 2 restricted universal quantifiers to both sides of an equivalence.
|- (ph <-> ps)   =>   |- (A.x e. A A.y e. B ph <-> A.x e. A A.y e. B ps)
Theorem	2rexbii 1716	Inference adding 2 restricted existential quantifiers to both sides of an equivalence.
|- (ph <-> ps)   =>   |- (E.x e. A E.y e. B ph <-> E.x e. A E.y e. B ps)
Theorem	ralbii2 1717	Inference adding different restricted universal quantifiers to each side of an equivalence.
|- ((x e. A -> ph) <-> (x e. B -> ps))   =>   |- (A.x e. A ph <-> A.x e. B ps)
Theorem	rexbii2 1718	Inference adding different restricted existential quantifiers to each side of an equivalence.
|- ((x e. A /\ ph) <-> (x e. B /\ ps))   =>   |- (E.x e. A ph <-> E.x e. B ps)
Theorem	ralbiia 1719	Inference adding restricted universal quantifier to both sides of an equivalence.
|- (x e. A -> (ph <-> ps))   =>   |- (A.x e. A ph <-> A.x e. A ps)
Theorem	rexbiia 1720	Inference adding restricted existential quantifier to both sides of an equivalence.
|- (x e. A -> (ph <-> ps))   =>   |- (E.x e. A ph <-> E.x e. A ps)
Theorem	2rexbiia 1721	Inference adding 2 restricted existential quantifiers to both sides of an equivalence.
|- ((x e. A /\ y e. B) -> (ph <-> ps))   =>   |- (E.x e. A E.y e. B ph <-> E.x e. A E.y e. B ps)
Theorem	r2al 1722	Double restricted universal quantification.
|- (A.x e. A A.y e. B ph <-> A.xA.y((x e. A /\ y e. B) -> ph))
Theorem	2ralbida 1723	Formula-building rule for restricted universal quantifier (deduction rule).
|- (ph -> A.xph)   &   |- (ph -> A.yph)   &   |- ((ph /\ (x e. A /\ y e. B)) -> (ps <-> ch))   =>   |- (ph -> (A.x e. A A.y e. B ps <-> A.x e. A A.y e. B ch))
Theorem	2ralbidva 1724	Formula-building rule for restricted universal quantifiers (deduction rule).
|- ((ph /\ (x e. A /\ y e. B)) -> (ps <-> ch))   =>   |- (ph -> (A.x e. A A.y e. B ps <-> A.x e. A A.y e. B ch))
Theorem	2rexbidva 1725	Formula-building rule for restricted existential quantifiers (deduction rule).
|- ((ph /\ (x e. A /\ y e. B)) -> (ps <-> ch))   =>   |- (ph -> (E.x e. A E.y e. B ps <-> E.x e. A E.y e. B ch))
Theorem	2ralbidv 1726	Formula-building rule for restricted universal quantifiers (deduction rule). (Distinct variable restriction on x and y removed by Szymon Jaroszewicz, 16-Mar-2006.)
|- (ph -> (ps <-> ch))   =>   |- (ph -> (A.x e. A A.y e. B ps <-> A.x e. A A.y e. B ch))
Theorem	2rexbidv 1727	Formula-building rule for restricted existential quantifiers (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> (E.x e. A E.y e. B ps <-> E.x e. A E.y e. B ch))
Theorem	rexralbidv 1728	Formula-building rule for restricted quantifiers (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> (E.x e. A A.y e. B ps <-> E.x e. A A.y e. B ch))
Theorem	ralinexa 1729	A transformation of restricted quantifiers and logical connectives.
|- (A.x e. A (ph -> -. ps) <-> -. E.x e. A (ph /\ ps))
Theorem	rexanali 1730	A transformation of restricted quantifiers and logical connectives.
|- (E.x e. A (ph /\ -. ps) <-> -. A.x e. A (ph -> ps))
Theorem	risset 1731	Two ways to say "A belongs to B."
|- (A e. B <-> E.x e. B x = A)
Theorem	hbral 1732	Bound-variable hypothesis builder for restricted quantification. (Distinct variable restriction on x and y was removed by David Abernethy, 13-Dec-2009.)
|- (y e. A -> A.x y e. A)   &   |- (ph -> A.xph)   =>   |- (A.y e. A ph -> A.xA.y e. A ph)
Theorem	hbra1 1733	x is not free in A.x e. Aph.
|- (A.x e. A ph -> A.xA.x e. A ph)
Theorem	hbrex 1734	Bound-variable hypothesis builder for restricted quantification. (Distinct variable restriction on x and y was removed by David Abernethy, 13-Dec-2009.)
|- (y e. A -> A.x y e. A)   &   |- (ph -> A.xph)   =>   |- (E.y e. A ph -> A.xE.y e. A ph)
Theorem	hbre1 1735	x is not free in E.x e. Aph.
|- (E.x e. A ph -> A.xE.x e. A ph)
Theorem	r3al 1736	Triple restricted universal quantification.
|- (A.x e. A A.y e. B A.z e. C ph <-> A.xA.yA.z((x e. A /\ y e. B /\ z e. C) -> ph))
Theorem	r2ex 1737	Double restricted existential quantification.
|- (E.x e. A E.y e. B ph <-> E.xE.y((x e. A /\ y e. B) /\ ph))
Theorem	alral 1738	Universal quantification implies restricted quantification.
|- (A.xph -> A.x e. A ph)
Theorem	rexex 1739	Restricted existence implies existence.
|- (E.x e. A ph -> E.xph)
Theorem	ra4 1740	Restricted specialization.
|- (A.x e. A ph -> (x e. A -> ph))
Theorem	ra4e 1741	Restricted specialization.
|- ((x e. A /\ ph) -> E.x e. A ph)
Theorem	ra42 1742	Restricted specialization.
|- (A.x e. A A.y e. B ph -> ((x e. A /\ y e. B) -> ph))
Theorem	rspec 1743	Specialization rule for restricted quantification.
|- A.x e. A ph   =>   |- (x e. A -> ph)
Theorem	rgen 1744	Generalization rule for restricted quantification.
|- (x e. A -> ph)   =>   |- A.x e. A ph
Theorem	rgen2a 1745	Generalization rule for restricted quantification. Note that x and y needn't be distinct.
|- ((x e. A /\ y e. A) -> ph)   =>   |- A.x e. A A.y e. A ph
Theorem	mprg 1746	Modus ponens combined with restricted generalization.
|- (A.x e. A ph -> ps)   &   |- (x e. A -> ph)   =>   |- ps
Theorem	mprgbir 1747	Modus ponens on biconditional combined with restricted generalization.
|- (ph <-> A.x e. A ps)   &   |- (x e. A -> ps)   =>   |- ph
Theorem	r19.20 1748	Distribution of restricted quantification over implication.
|- (A.x e. A (ph -> ps) -> (A.x e. A ph -> A.x e. A ps))
Theorem	r19.20i2 1749	Inference quantifying both antecedent and consequent.
|- ((x e. A -> ph) -> (x e. B -> ps))   =>   |- (A.x e. A ph -> A.x e. B ps)
Theorem	r19.20i 1750	Inference quantifying both antecedent and consequent.
|- (x e. A -> (ph -> ps))   =>   |- (A.x e. A ph -> A.x e. A ps)
Theorem	r19.20ia 1751	Inference quantifying both antecedent and consequent.
|- ((x e. A /\ ph) -> ps)   =>   |- (A.x e. A ph -> A.x e. A ps)
Theorem	r19.20si 1752	Inference quantifying both antecedent and consequent, with strong hypothesis.
|- (ph -> ps)   =>   |- (A.x e. A ph -> A.x e. A ps)
Theorem	r19.20sii 1753	Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis.
|- (ph -> (ps -> ch))   =>   |- (A.x e. A ph -> (A.x e. A ps -> A.x e. A ch))
Theorem	r19.20da 1754	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90.
|- (ph -> A.xph)   &   |- ((ph /\ x e. A) -> (ps -> ch))   =>   |- (ph -> (A.x e. A ps -> A.x e. A ch))
Theorem	r19.20dva 1755	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90.
|- ((ph /\ x e. A) -> (ps -> ch))   =>   |- (ph -> (A.x e. A ps -> A.x e. A ch))
Theorem	r19.20sdv 1756	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90.
|- (ph -> (ps -> ch))   =>   |- (ph -> (A.x e. A ps -> A.x e. A ch))
Theorem	r19.20dv2 1757	Inference quantifying both antecedent and consequent.
|- (ph -> ((x e. A -> ps) -> (x e. B -> ch)))   =>   |- (ph -> (A.x e. A ps -> A.x e. B ch))
Theorem	r19.21ai 1758	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
|- (ph -> A.xph)   &   |- (ph -> (x e. A -> ps))   =>   |- (ph -> A.x e. A ps)
Theorem	r19.21aiv 1759	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
|- (ph -> (x e. A -> ps))   =>   |- (ph -> A.x e. A ps)
Theorem	r19.21aiva 1760	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
|- ((ph /\ x e. A) -> ps)   =>   |- (ph -> A.x e. A ps)
Theorem	r19.21t 1761	Theorem 19.21 of [Margaris] p. 90 with restricted quantifiers (closed theorem version).
|- (A.x(ph -> A.xph) -> (A.x e. A (ph -> ps) <-> (ph -> A.x e. A ps)))
Theorem	r19.21v 1762	Theorem 19.21 of [Margaris] p. 90 with restricted quantifiers.
|- (A.x e. A (ph -> ps) <-> (ph -> A.x e. A ps))
Theorem	r19.21ad 1763	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
|- (ph -> A.xph)   &   |- (ps -> A.xps)   &   |- (ph -> (ps -> (x e. A -> ch)))   =>   |- (ph -> (ps -> A.x e. A ch))
Theorem	r19.21adv 1764	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
|- (ph -> (ps -> (x e. A -> ch)))   =>   |- (ph -> (ps -> A.x e. A ch))
Theorem	r19.21adva 1765	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
|- ((ph /\ x e. A) -> (ps -> ch))   =>   |- (ph -> (ps -> A.x e. A ch))
Theorem	r19.21aivv 1766	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.)
|- (ph -> ((x e. A /\ y e. B) -> ps))   =>   |- (ph -> A.x e. A A.y e. B ps)
Theorem	r19.21advv 1767	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.)
|- (ph -> (ps -> ((x e. A /\ y e. B) -> ch)))   =>   |- (ph -> (ps -> A.x e. A A.y e. B ch))
Theorem	r19.21advva 1768	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.)
|- ((ph /\ (x e. A /\ y e. B)) -> (ps -> ch))   =>   |- (ph -> (ps -> A.x e. A A.y e. B ch))
Theorem	rgen2 1769	Generalization rule for restricted quantification.
|- ((x e. A /\ y e. B) -> ph)   =>   |- A.x e. A A.y e. B ph
Theorem	rgen3 1770	Generalization rule for restricted quantification.
|- ((x e. A /\ y e. B /\ z e. C) -> ph)   =>   |- A.x e. A A.y e. B A.z e. C ph
Theorem	r19.21bi 1771	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
|- (ph -> A.x e. A ps)   =>   |- ((ph /\ x e. A) -> ps)
Theorem	rspec2 1772	Specialization rule for restricted quantification.
|- A.x e. A A.y e. B ph   =>   |- ((x e. A /\ y e. B) -> ph)
Theorem	rspec3 1773	Specialization rule for restricted quantification.
|- A.x e. A A.y e. B A.z e. C ph   =>   |- ((x e. A /\ y e. B /\ z e. C) -> ph)
Theorem	r19.21be 1774	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
|- (ph -> A.x e. A ps)   =>   |- A.x e. A (ph -> ps)
Theorem	nrex 1775	Inference adding restricted existential quantifier to negated wff.
|- (x e. A -> -. ps)   =>   |- -. E.x e. A ps
Theorem	nrexdv 1776	Deduction adding restricted existential quantifier to negated wff.
|- ((ph /\ x e. A) -> -. ps)   =>   |- (ph -> -. E.x e. A ps)
Theorem	r19.22 1777	Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.)
|- (A.x e. A (ph -> ps) -> (E.x e. A ph -> E.x e. A ps))
Theorem	r19.22i 1778	Inference quantifying both antecedent and consequent.
|- (x e. A -> (ph -> ps))   =>   |- (E.x e. A ph -> E.x e. A ps)
Theorem	r19.22i2 1779	Inference quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90.
|- ((x e. A /\ ph) -> (x e. B /\ ps))   =>   |- (E.x e. A ph -> E.x e. B ps)
Theorem	r19.22si 1780	Inference quantifying both antecedent and consequent.
|- (ph -> ps)   =>   |- (E.x e. A ph -> E.x e. A ps)
Theorem	r19.22d 1781	Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.)
|- (ph -> A.xph)   &   |- (ph -> (x e. A -> (ps -> ch)))   =>   |- (ph -> (E.x e. A ps -> E.x e. A ch))
Theorem	r19.22dv2 1782	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90.
|- (ph -> ((x e. A /\ ps) -> (x e. B /\ ch)))   =>   |- (ph -> (E.x e. A ps -> E.x e. B ch))
Theorem	r19.22dv 1783	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90.
|- (ph -> (x e. A -> (ps -> ch)))   =>   |- (ph -> (E.x e. A ps -> E.x e. A ch))
Theorem	r19.22sdv 1784	Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.)
|- (ph -> (ps -> ch))   =>   |- (ph -> (E.x e. A ps -> E.x e. A ch))
Theorem	r19.22dva 1785	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90.
|- ((ph /\ x e. A) -> (ps -> ch))   =>   |- (ph -> (E.x e. A ps -> E.x e. A ch))
Theorem	r19.12 1786	Theorem 19.12 of [Margaris] p. 89 with restricted quantifiers.
|- (E.x e. A A.y e. B ph -> A.y e. B E.x e. A ph)
Theorem	r19.23v 1787	Theorem 19.23 of [Margaris] p. 90 with restricted quantifiers.
|- (A.x e. A (ph -> ps) <-> (E.x e. A ph -> ps))
Theorem	r19.23ai 1788	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
|- (ps -> A.xps)   &   |- (x e. A -> (ph -> ps))   =>   |- (E.x e. A ph -> ps)
Theorem	r19.23aiv 1789	Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.)
|- (x e. A -> (ph -> ps))   =>   |- (E.x e. A ph -> ps)
Theorem	r19.23aiva 1790	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version).
|- ((x e. A /\ ph) -> ps)   =>   |- (E.x e. A ph -> ps)
Theorem	r19.23ad 1791	Deduction from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version).
|- (ph -> A.xph)   &   |- (ch -> A.xch)   &   |- (ph -> (x e. A -> (ps -> ch)))   =>   |- (ph -> (E.x e. A ps -> ch))
Theorem	r19.23adv 1792	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (The proof was shortened by Eric Schmidt, 22-Dec-2006.)
|- (ph -> (x e. A -> (ps -> ch)))   =>   |- (ph -> (E.x e. A ps -> ch))
Theorem	r19.23adva 1793	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version).
|- ((ph /\ x e. A) -> (ps -> ch))   =>   |- (ph -> (E.x e. A ps -> ch))
Theorem	r19.23aivv 1794	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version).
|- ((x e. A /\ y e. B) -> (ph -> ps))   =>   |- (E.x e. A E.y e. B ph -> ps)
Theorem	r19.23advv 1795	Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.)
|- (ph -> ((x e. A /\ y e. B) -> (ps -> ch)))   =>   |- (ph -> (E.x e. A E.y e. B ps -> ch))
Theorem	r19.26 1796	Theorem 19.26 of [Margaris] p. 90 with restricted quantifiers.
|- (A.x e. A (ph /\ ps) <-> (A.x e. A ph /\ A.x e. A ps))
Theorem	r19.26-2 1797	Theorem 19.26 of [Margaris] p. 90 with 2 restricted quantifiers.
|- (A.x e. A A.y e. B (ph /\ ps) <-> (A.x e. A A.y e. B ph /\ A.x e. A A.y e. B ps))
Theorem	r19.26m 1798	Theorem 19.26 of [Margaris] p. 90 with mixed quantifiers.
|- (A.x((x e. A -> ph) /\ (x e. B -> ps)) <-> (A.x e. A ph /\ A.x e. B ps))
Theorem	r19.15 1799	Distribute a restricted universal quantifier over a biconditional. Theorem 19.15 of [Margaris] p. 90 with restricted quantification.
|- (A.x e. A (ph <-> ps) -> (A.x e. A ph <-> A.x e. A ps))
Theorem	r19.27av 1800	Restricted version of one direction of Theorem 19.27 of [Margaris] p. 90. (The other direction doesn't hold when A is empty.)
|- ((A.x e. A ph /\ ps) -> A.x e. A (ph /\ ps))