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  2348  ee4anv  2349  ee4anvOLD  2350  2exsb  2359  cbvex4v  2414  2sb5rf  2471  sbel2x  2473  2mo2  2641  r3ex  3177  reeanlem  3209  rexcomf  3279  cgsex4g  3497  ceqsex3v  3506  ceqsex4v  3507  ceqsex8v  3509  copsexgw  5453  copsexg  5454  copsex2g  5456  vopelopabsb  5492  opabn0  5516  elxp2  5665  rabxp  5689  elxp3  5707  elvv  5716  elvvv  5717  copsex2gb  5772  elcnv2  5844  cnvuni  5853  cnvopab  6113  xpdifid  6144  coass  6241  fununi  6594  dfmpt3  6655  tpres  7178  dfoprab2  7450  cbvoprab3v  7484  dmoprab  7495  rnoprab  7497  mpomptx  7505  resoprab  7510  elrnmpores  7530  ov3  7555  ov6g  7556  uniuni  7741  opabex3rd  7948  oprabex3  7959  oeeu  8570  xpassen  9040  sbthfilem  9168  zorn2lem6  10461  ltresr  11100  axaddf  11105  axmulf  11106  hashfun  14409  hash2prb  14444  5oalem7  31596  mpomptxf  32608  eulerpartlemgvv  34374  bnj600  34916  bnj916  34930  bnj983  34948  bnj986  34952  bnj996  34953  bnj1021  34963  dfacycgr1  35138  satfv1  35357  elima4  35770  brtxp2  35876  brpprod3a  35881  brpprod3b  35882  elfuns  35910  brcart  35927  brimg  35932  brapply  35933  brsuccf  35936  brrestrict  35944  dfrdg4  35946  ellines  36147  bj-cbvex4vv  36800  itg2addnclem3  37674  brxrn2  38364  dfxrn2  38365  ecxrn  38380  inxpxrn  38388  rnxrn  38391  dmqsblocks  38852  dalem20  39694  dvhopellsm  41118  diblsmopel  41172  ralopabb  43407  en2pr  43543  pm11.52  44383  pm11.6  44388  pm11.7  44392  opelopab4  44548  stoweidlem35  46040  fundcmpsurbijinj  47415  mpomptx2  48327