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  3492  ceqsex4v  3493  ceqsex8v  3495  copsexgw  5430  copsexg  5431  copsex2g  5433  vopelopabsb  5469  opabn0  5493  elxp2  5640  rabxp  5664  elxp3  5682  elvv  5691  elvvv  5692  copsex2gb  5746  elcnv2  5817  cnvuni  5826  cnvopab  6084  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  10389  ltresr  11028  axaddf  11033  axmulf  11034  hashfun  14341  hash2prb  14376  5oalem7  31635  mpomptxf  32654  eulerpartlemgvv  34384  bnj600  34926  bnj916  34940  bnj983  34958  bnj986  34962  bnj996  34963  bnj1021  34973  dfacycgr1  35176  satfv1  35395  elima4  35808  brtxp2  35914  brpprod3a  35919  brpprod3b  35920  elfuns  35948  brcart  35965  brimg  35970  brapply  35971  brsuccf  35974  brrestrict  35982  dfrdg4  35984  ellines  36185  bj-cbvex4vv  36838  itg2addnclem3  37712  brxrn2  38402  dfxrn2  38403  ecxrn  38418  inxpxrn  38426  rnxrn  38429  dmqsblocks  38890  dalem20  39731  dvhopellsm  41155  diblsmopel  41209  ralopabb  43443  en2pr  43579  pm11.52  44419  pm11.6  44424  pm11.7  44428  opelopab4  44583  stoweidlem35  46072  fundcmpsurbijinj  47440  mpomptx2  48365