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  2352  ee4anv  2353  ee4anvOLD  2354  2exsb  2363  cbvex4v  2420  2sb5rf  2477  sbel2x  2479  2mo2  2647  r3ex  3184  reeanlem  3216  rexcomf  3287  cgsex4g  3512  ceqsex3v  3521  ceqsex4v  3522  ceqsex8v  3524  copsexgw  5470  copsexg  5471  copsex2g  5473  vopelopabsb  5509  opabn0  5533  elxp2  5683  rabxp  5707  elxp3  5725  elvv  5734  elvvv  5735  copsex2gb  5790  elcnv2  5862  cnvuni  5871  cnvopab  6131  xpdifid  6162  coass  6259  fununi  6616  dfmpt3  6677  tpres  7198  dfoprab2  7470  cbvoprab3v  7504  dmoprab  7515  rnoprab  7517  mpomptx  7525  resoprab  7530  elrnmpores  7550  ov3  7575  ov6g  7576  uniuni  7761  opabex3rd  7970  oprabex3  7981  wfrlem4OLD  8331  oeeu  8620  xpassen  9085  sbthfilem  9217  zorn2lem6  10520  ltresr  11159  axaddf  11164  axmulf  11165  hashfun  14460  hash2prb  14495  5oalem7  31646  mpomptxf  32660  eulerpartlemgvv  34413  bnj600  34955  bnj916  34969  bnj983  34987  bnj986  34991  bnj996  34992  bnj1021  35002  dfacycgr1  35171  satfv1  35390  elima4  35798  brtxp2  35904  brpprod3a  35909  brpprod3b  35910  elfuns  35938  brcart  35955  brimg  35960  brapply  35961  brsuccf  35964  brrestrict  35972  dfrdg4  35974  ellines  36175  bj-cbvex4vv  36828  itg2addnclem3  37702  brxrn2  38398  dfxrn2  38399  ecxrn  38410  inxpxrn  38418  rnxrn  38421  dalem20  39717  dvhopellsm  41141  diblsmopel  41195  ralopabb  43402  en2pr  43538  pm11.52  44378  pm11.6  44383  pm11.7  44387  opelopab4  44543  stoweidlem35  46031  fundcmpsurbijinj  47391  mpomptx2  48277