Theorem 2exbii 1852

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

Syntax hints:   ↔ wb 205  ∃wex 1783

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

This theorem depends on definitions:  df-bi 206  df-ex 1784

This theorem is referenced by:  3exbii  1853  2exanali  1864  4exdistrv  1961  3exdistr  1965  cbvex4vw  2046  eeeanv  2350  ee4anv  2351  2exsb  2358  cbvex4v  2415  2sb5rf  2472  sbel2x  2474  2mo2  2649  rexcomf  3283  reeanlem  3290  ceqsex3v  3474  ceqsex4v  3475  ceqsex8v  3477  copsexgw  5398  copsexg  5399  copsex2g  5401  vopelopabsb  5435  opabn0  5459  elxp2  5604  rabxp  5626  elxp3  5644  elvv  5652  elvvv  5653  copsex2gb  5705  elcnv2  5775  cnvuni  5784  xpdifid  6060  coass  6158  fununi  6493  dfmpt3  6551  tpres  7058  dfoprab2  7311  dmoprab  7354  rnoprab  7356  mpomptx  7365  resoprab  7370  elrnmpores  7389  ov3  7413  ov6g  7414  uniuni  7590  opabex3rd  7782  oprabex3  7793  wfrlem4OLD  8114  oeeu  8396  xpassen  8806  sbthfilem  8941  zorn2lem6  10188  ltresr  10827  axaddf  10832  axmulf  10833  hashfun  14080  hash2prb  14114  5oalem7  29923  mpomptxf  30918  eulerpartlemgvv  32243  bnj600  32799  bnj916  32813  bnj983  32831  bnj986  32835  bnj996  32836  bnj1021  32846  dfacycgr1  33006  satfv1  33225  elima4  33656  brtxp2  34110  brpprod3a  34115  brpprod3b  34116  elfuns  34144  brcart  34161  brimg  34166  brapply  34167  brsuccf  34170  brrestrict  34178  dfrdg4  34180  ellines  34381  bj-cbvex4vv  34914  itg2addnclem3  35757  brxrn2  36432  dfxrn2  36433  ecxrn  36444  inxpxrn  36448  rnxrn  36451  dalem20  37634  dvhopellsm  39058  diblsmopel  39112  en2pr  41043  pm11.52  41894  pm11.6  41899  pm11.7  41903  opelopab4  42060  stoweidlem35  43466  fundcmpsurbijinj  44750  mpomptx2  45558