Theorem 19.42vv 1907

Description: Theorem 19.42 of [Margaris] p. 90 with 2 quantifiers. (Contributed by NM, 16-Mar-1995.)

Assertion

Ref	Expression
19.42vv	|- (E.xE.y(ph /\ ps) <-> (ph /\ E.xE.yps))

Distinct variable groups:   ph,x   ph,y

Allowed substitution hints:   ps(x,y)

Proof of Theorem 19.42vv

Step	Hyp	Ref	Expression
1		exdistr 1906	. 2 |- (E.xE.y(ph /\ ps) <-> E.x(ph /\ E.yps))
2		19.42v 1905	. 2 |- (E.x(ph /\ E.yps) <-> (ph /\ E.xE.yps))
3	1, 2	bitri 240	1 |- (E.xE.y(ph /\ ps) <-> (ph /\ E.xE.yps))

Syntax hints:   <-> wb 176   /\ wa 358  E.wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545

This theorem is referenced by:  19.42vvv  1908  exdistr2  1909  3exdistr  1910  ceqsex3v  2898  ceqsex4v  2899  ceqsex8v  2901  otkelins2kg  4254  otkelins3kg  4255  opkelcokg  4262  sikexlem  4296  insklem  4305  elswap  4741  dmsi  5520  dfoprab2  5559  resoprab  5582  ov3  5600  ov6g  5601  brpprod  5840  dmpprod  5841  lecex  6116  ce0nnul  6178