Theorem 2exbii 1872

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 1871	. 2 ⊢ (∃𝑦𝜑 ↔ ∃𝑦𝜓)
3	2	exbii 1871	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓)

Syntax hints:   ↔ wb 209  ∃wex 1802

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

This theorem depends on definitions:  df-bi 210  df-ex 1803

This theorem is referenced by:  3exbii  1873  2exanali  1883  4exdistrv  1979  3exdistr  1983  cbvex4vw  2065  eeeanv  2384  ee4anv  2385  ee4anvOLD  2386  2exsb  2394  cbvex4v  2449  2sb5rf  2506  sbel2x  2508  2mo2  2677  r3ex  3204  reeanlem  3236  rexcomf  3304  cgsex4g  3503  ceqsex3v  3509  ceqsex4v  3510  ceqsex8v  3512  copsexgw  5463  copsexgwOLD  5464  copsexg  5465  copsex2g  5467  vopelopabsb  5504  opabn0  5529  elxp2  5676  rabxp  5700  elxp3  5718  elvv  5727  elvvv  5728  copsex2gb  5784  elcnv2  5854  cnvuni  5867  cnvopab  6128  xpdifid  6157  xpdifcnvepel  6158  coass  6257  fununi  6600  dfmpt3  6659  tpres  7189  dfoprab2  7458  cbvoprab3v  7492  dmoprab  7503  rnoprab  7505  mpomptx  7513  resoprab  7518  elrnmpores  7538  ov3  7563  ov6g  7564  uniuni  7749  opabex3rd  7951  oprabex3  7962  oeeu  8577  xpassen  9047  sbthfilem  9170  zorn2lem6  10473  ltresr  11113  axaddf  11118  axmulf  11119  hashfun  14464  hash2prb  14499  5oalem7  31921  mpomptxf  32935  eulerpartlemgvv  34683  bnj600  35224  bnj916  35238  bnj983  35256  bnj986  35260  bnj996  35261  bnj1021  35271  dfacycgr1  35507  satfv1  35726  elima4  36139  brtxp2  36242  brpprod3a  36247  brpprod3b  36248  elfuns  36276  brcart  36293  brimg  36298  brapply  36299  lemsuccf  36302  brrestrict  36312  dfrdg4  36314  ellines  36515  bj-cbvex4vv  37302  copsex2gd  37642  itg2addnclem3  38184  brxrn2  38895  dfxrn2  38896  ecxrn  38917  inxpxrn  38929  rnxrn  38932  dmqsblocks  39478  dalem20  40329  dvhopellsm  41753  diblsmopel  41807  ralopabb  43999  en2pr  44135  pm11.52  44961  pm11.6  44966  pm11.7  44970  opelopab4  45125  stoweidlem35  46607  fundcmpsurbijinj  48014  mpomptx2  48966