Theorem 2exbii 1850

Description: Inference adding two existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.)

Hypothesis

Ref	Expression
2exbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
2exbii	⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓)

Proof of Theorem 2exbii

Step	Hyp	Ref	Expression
1		2exbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	exbii 1849	. 2 ⊢ (∃𝑦𝜑 ↔ ∃𝑦𝜓)
3	2	exbii 1849	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓)

Syntax hints:   ↔ wb 206  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810

This theorem depends on definitions:  df-bi 207  df-ex 1781

This theorem is referenced by:  3exbii  1851  2exanali  1861  4exdistrv  1957  3exdistr  1961  cbvex4vw  2043  eeeanv  2350  ee4anv  2351  ee4anvOLD  2352  2exsb  2360  cbvex4v  2415  2sb5rf  2472  sbel2x  2474  2mo2  2642  r3ex  3171  reeanlem  3203  rexcomf  3271  cgsex4g  3483  ceqsex3v  3491  ceqsex4v  3492  ceqsex8v  3494  copsexgw  5428  copsexg  5429  copsex2g  5431  vopelopabsb  5467  opabn0  5491  elxp2  5638  rabxp  5662  elxp3  5680  elvv  5689  elvvv  5690  copsex2gb  5745  elcnv2  5816  cnvuni  5825  cnvopab  6083  xpdifid  6115  coass  6213  fununi  6556  dfmpt3  6615  tpres  7135  dfoprab2  7404  cbvoprab3v  7438  dmoprab  7449  rnoprab  7451  mpomptx  7459  resoprab  7464  elrnmpores  7484  ov3  7509  ov6g  7510  uniuni  7695  opabex3rd  7898  oprabex3  7909  oeeu  8518  xpassen  8984  sbthfilem  9107  zorn2lem6  10392  ltresr  11031  axaddf  11036  axmulf  11037  hashfun  14344  hash2prb  14379  5oalem7  31640  mpomptxf  32659  eulerpartlemgvv  34389  bnj600  34931  bnj916  34945  bnj983  34963  bnj986  34967  bnj996  34968  bnj1021  34978  dfacycgr1  35188  satfv1  35407  elima4  35820  brtxp2  35923  brpprod3a  35928  brpprod3b  35929  elfuns  35957  brcart  35974  brimg  35979  brapply  35980  lemsuccf  35983  brrestrict  35993  dfrdg4  35995  ellines  36196  bj-cbvex4vv  36849  itg2addnclem3  37712  brxrn2  38407  dfxrn2  38408  ecxrn  38429  inxpxrn  38441  rnxrn  38444  dmqsblocks  38950  dalem20  39791  dvhopellsm  41215  diblsmopel  41269  ralopabb  43503  en2pr  43639  pm11.52  44479  pm11.6  44484  pm11.7  44488  opelopab4  44643  stoweidlem35  46132  fundcmpsurbijinj  47509  mpomptx2  48434