Theorem 2exbii 1882

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

This proof depends on syntax axioms:   ↔ wb 209  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  3exbii  1883  2exanali  1893  4exdistrv  1991  3exdistr  1995  cbvex4vw  2077  eeeanv  2383  ee4anv  2384  2exsb  2392  cbvex4v  2447  2sb5rf  2504  sbel2x  2506  2mo2  2675  r3ex  3205  reeanlem  3237  rexcomf  3305  cgsex4g  3500  ceqsex3v  3506  ceqsex4v  3507  ceqsex8v  3509  copsexgw  5464  copsexgwOLD  5465  copsexg  5466  copsex2g  5469  vopelopabsb  5507  opabn0  5532  elxp2  5679  rabxp  5703  elxp3  5721  elvvOLD  5731  elvvv  5732  copsex2gb  5789  relopabi  5805  elcnv2  5862  cnvuni  5875  cnvopab  6143  xpdifid  6171  xpdifcnvepel  6172  coassOLD  6285  fununi  6637  dfmpt3  6695  tpres  7230  dfoprab2  7501  cbvoprab3v  7535  dmoprab  7546  rnoprab  7548  mpomptx  7556  resoprab  7561  elrnmpores  7582  ov3  7607  ov6g  7608  uniuni  7800  opabex3rd  8002  oprabex3  8013  oeeu  8640  xpassen  9118  sbthfilem  9241  zorn2lem6  10606  ltresr  11252  axaddf  11257  axmulf  11258  hashfun  14609  hash2prb  14644  degenmgm2nfun  19168  dfric2  20787  dfacycgr1  30780  5oalem7  32292  mpomptxf  33343  eulerpartlemgvv  35078  bnj600  35619  bnj916  35633  bnj983  35651  bnj986  35655  bnj996  35656  bnj1021  35666  satfv1  36295  mirimanofffr  36629  elima4  36718  brtxp2  36821  brpprod3a  36826  brpprod3b  36827  elfuns  36855  brcart  36872  brimg  36877  brapply  36878  lemsuccf  36881  brrestrict  36891  dfrdg4  36893  ellines  37095  bj-cbvex4vv  37895  copsex2gd  38251  itg2addnclem3  38783  brxrn2  39508  dfxrn2  39509  ecxrn  39530  inxpxrn  39542  rnxrn  39545  dmqsblocks  40091  dalem20  40942  dvhopellsm  42366  diblsmopel  42420  ralopabb  44604  en2pr  44740  pm11.52  45563  pm11.6  45568  pm11.7  45572  opelopab4  45725  stoweidlem35  47250  fundcmpsurbijinj  48697  mpomptx2  49652