Theorem 2exbii 1849

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

Syntax hints:   ↔ wb 206  ∃wex 1779

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

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

This theorem is referenced by:  3exbii  1850  2exanali  1860  4exdistrv  1956  3exdistr  1960  cbvex4vw  2042  eeeanv  2348  ee4anv  2349  ee4anvOLD  2350  2exsb  2358  cbvex4v  2413  2sb5rf  2470  sbel2x  2472  2mo2  2640  r3ex  3168  reeanlem  3200  rexcomf  3269  cgsex4g  3485  ceqsex3v  3494  ceqsex4v  3495  ceqsex8v  3497  copsexgw  5437  copsexg  5438  copsex2g  5440  vopelopabsb  5476  opabn0  5500  elxp2  5647  rabxp  5671  elxp3  5689  elvv  5698  elvvv  5699  copsex2gb  5753  elcnv2  5824  cnvuni  5833  cnvopab  6090  xpdifid  6121  coass  6218  fununi  6561  dfmpt3  6620  tpres  7141  dfoprab2  7411  cbvoprab3v  7445  dmoprab  7456  rnoprab  7458  mpomptx  7466  resoprab  7471  elrnmpores  7491  ov3  7516  ov6g  7517  uniuni  7702  opabex3rd  7908  oprabex3  7919  oeeu  8528  xpassen  8995  sbthfilem  9122  zorn2lem6  10414  ltresr  11053  axaddf  11058  axmulf  11059  hashfun  14362  hash2prb  14397  5oalem7  31622  mpomptxf  32634  eulerpartlemgvv  34343  bnj600  34885  bnj916  34899  bnj983  34917  bnj986  34921  bnj996  34922  bnj1021  34932  dfacycgr1  35116  satfv1  35335  elima4  35748  brtxp2  35854  brpprod3a  35859  brpprod3b  35860  elfuns  35888  brcart  35905  brimg  35910  brapply  35911  brsuccf  35914  brrestrict  35922  dfrdg4  35924  ellines  36125  bj-cbvex4vv  36778  itg2addnclem3  37652  brxrn2  38342  dfxrn2  38343  ecxrn  38358  inxpxrn  38366  rnxrn  38369  dmqsblocks  38830  dalem20  39672  dvhopellsm  41096  diblsmopel  41150  ralopabb  43384  en2pr  43520  pm11.52  44360  pm11.6  44365  pm11.7  44369  opelopab4  44525  stoweidlem35  46017  fundcmpsurbijinj  47395  mpomptx2  48320