Theorem 2exbii 1851

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

Syntax hints:   ↔ wb 206  ∃wex 1781

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

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

This theorem is referenced by:  3exbii  1852  2exanali  1862  4exdistrv  1958  3exdistr  1962  cbvex4vw  2044  eeeanv  2354  ee4anv  2355  ee4anvOLD  2356  2exsb  2364  cbvex4v  2419  2sb5rf  2476  sbel2x  2478  2mo2  2647  r3ex  3176  reeanlem  3208  rexcomf  3276  cgsex4g  3476  ceqsex3v  3483  ceqsex4v  3484  ceqsex8v  3486  copsexgw  5443  copsexgwOLD  5444  copsexg  5445  copsex2g  5447  vopelopabsb  5484  opabn0  5508  elxp2  5655  rabxp  5679  elxp3  5697  elvv  5706  elvvv  5707  copsex2gb  5762  elcnv2  5832  cnvuni  5841  cnvopab  6100  xpdifid  6132  coass  6230  fununi  6573  dfmpt3  6632  tpres  7156  dfoprab2  7425  cbvoprab3v  7459  dmoprab  7470  rnoprab  7472  mpomptx  7480  resoprab  7485  elrnmpores  7505  ov3  7530  ov6g  7531  uniuni  7716  opabex3rd  7919  oprabex3  7930  oeeu  8539  xpassen  9009  sbthfilem  9132  zorn2lem6  10423  ltresr  11063  axaddf  11068  axmulf  11069  hashfun  14399  hash2prb  14434  5oalem7  31731  mpomptxf  32751  eulerpartlemgvv  34520  bnj600  35061  bnj916  35075  bnj983  35093  bnj986  35097  bnj996  35098  bnj1021  35108  dfacycgr1  35326  satfv1  35545  elima4  35958  brtxp2  36061  brpprod3a  36066  brpprod3b  36067  elfuns  36095  brcart  36112  brimg  36117  brapply  36118  lemsuccf  36121  brrestrict  36131  dfrdg4  36133  ellines  36334  bj-cbvex4vv  37112  copsex2gd  37452  itg2addnclem3  37994  brxrn2  38705  dfxrn2  38706  ecxrn  38727  inxpxrn  38739  rnxrn  38742  dmqsblocks  39288  dalem20  40139  dvhopellsm  41563  diblsmopel  41617  ralopabb  43838  en2pr  43974  pm11.52  44814  pm11.6  44819  pm11.7  44823  opelopab4  44978  stoweidlem35  46463  fundcmpsurbijinj  47870  mpomptx2  48811