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  1989  3exdistr  1993  cbvex4vw  2075  eeeanv  2380  ee4anv  2381  ee4anvOLD  2382  2exsb  2390  cbvex4v  2445  2sb5rf  2502  sbel2x  2504  2mo2  2673  r3ex  3202  reeanlem  3234  rexcomf  3302  cgsex4g  3497  ceqsex3v  3503  ceqsex4v  3504  ceqsex8v  3506  copsexgw  5460  copsexgwOLD  5461  copsexg  5462  copsex2g  5465  vopelopabsb  5503  opabn0  5528  elxp2  5675  rabxp  5699  elxp3  5717  elvv  5726  elvvv  5727  copsex2gb  5784  elcnv2  5855  cnvuni  5868  cnvopab  6129  xpdifid  6158  xpdifcnvepel  6159  coass  6260  fununi  6607  dfmpt3  6665  tpres  7199  dfoprab2  7470  cbvoprab3v  7504  dmoprab  7515  rnoprab  7517  mpomptx  7525  resoprab  7530  elrnmpores  7550  ov3  7575  ov6g  7576  uniuni  7765  opabex3rd  7967  oprabex3  7978  oeeu  8596  xpassen  9074  sbthfilem  9197  zorn2lem6  10560  ltresr  11206  axaddf  11211  axmulf  11212  hashfun  14562  hash2prb  14597  degenmgm2nfun  19119  dfric2  20737  dfacycgr1  30732  5oalem7  32244  mpomptxf  33254  eulerpartlemgvv  34991  bnj600  35532  bnj916  35546  bnj983  35564  bnj986  35568  bnj996  35569  bnj1021  35579  satfv1  36097  elima4  36510  brtxp2  36613  brpprod3a  36618  brpprod3b  36619  elfuns  36647  brcart  36664  brimg  36669  brapply  36670  lemsuccf  36673  brrestrict  36683  dfrdg4  36685  ellines  36887  bj-cbvex4vv  37687  copsex2gd  38027  itg2addnclem3  38559  brxrn2  39284  dfxrn2  39285  ecxrn  39306  inxpxrn  39318  rnxrn  39321  dmqsblocks  39867  dalem20  40718  dvhopellsm  42142  diblsmopel  42196  ralopabb  44370  en2pr  44506  pm11.52  45330  pm11.6  45335  pm11.7  45339  opelopab4  45493  stoweidlem35  46989  fundcmpsurbijinj  48436  mpomptx2  49391