Theorem 2exbii 1846

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

Syntax hints:   ↔ wb 206  ∃wex 1776

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

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

This theorem is referenced by:  3exbii  1847  2exanali  1858  4exdistrv  1954  3exdistr  1958  cbvex4vw  2039  eeeanv  2351  ee4anv  2352  2exsb  2361  cbvex4v  2418  2sb5rf  2475  sbel2x  2477  2mo2  2645  r3ex  3196  reeanlem  3226  rexcomf  3301  cgsex4g  3526  ceqsex3v  3537  ceqsex4v  3538  ceqsex8v  3540  copsexgw  5501  copsexg  5502  copsex2g  5504  vopelopabsb  5539  opabn0  5563  elxp2  5713  rabxp  5737  elxp3  5755  elvv  5763  elvvv  5764  copsex2gb  5819  elcnv2  5891  cnvuni  5900  cnvopab  6160  xpdifid  6190  coass  6287  fununi  6643  dfmpt3  6703  tpres  7221  dfoprab2  7491  cbvoprab3v  7525  dmoprab  7535  rnoprab  7537  mpomptx  7546  resoprab  7551  elrnmpores  7571  ov3  7596  ov6g  7597  uniuni  7781  opabex3rd  7990  oprabex3  8001  wfrlem4OLD  8351  oeeu  8640  xpassen  9105  sbthfilem  9236  zorn2lem6  10539  ltresr  11178  axaddf  11183  axmulf  11184  hashfun  14473  hash2prb  14508  5oalem7  31689  mpomptxf  32694  eulerpartlemgvv  34358  bnj600  34912  bnj916  34926  bnj983  34944  bnj986  34948  bnj996  34949  bnj1021  34959  dfacycgr1  35129  satfv1  35348  elima4  35757  brtxp2  35863  brpprod3a  35868  brpprod3b  35869  elfuns  35897  brcart  35914  brimg  35919  brapply  35920  brsuccf  35923  brrestrict  35931  dfrdg4  35933  ellines  36134  bj-cbvex4vv  36788  itg2addnclem3  37660  brxrn2  38357  dfxrn2  38358  ecxrn  38369  inxpxrn  38377  rnxrn  38380  dalem20  39676  dvhopellsm  41100  diblsmopel  41154  ralopabb  43401  en2pr  43537  pm11.52  44383  pm11.6  44388  pm11.7  44392  opelopab4  44549  stoweidlem35  45991  fundcmpsurbijinj  47335  mpomptx2  48180