Theorem 2exbii 1843

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

Syntax hints:   ↔ wb 208  ∃wex 1774

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

This theorem depends on definitions:  df-bi 209  df-ex 1775

This theorem is referenced by:  3exbii  1844  2exanali  1854  4exdistrv  1951  3exdistr  1956  cbvex4vw  2043  eeeanv  2365  ee4anv  2366  2exsb  2373  cbvex4v  2431  2sb5rf  2490  sbel2x  2492  2mo2  2726  rexcomOLD  3354  rexcomf  3356  reeanlem  3364  ceqsex3v  3544  ceqsex4v  3545  ceqsex8v  3547  copsexgw  5372  copsexg  5373  opelopabsbALT  5407  opabn0  5431  elxp2  5572  rabxp  5593  elxp3  5611  elvv  5619  elvvv  5620  copsex2gb  5672  elcnv2  5741  cnvuni  5750  xpdifid  6018  coass  6111  fununi  6422  dfmpt3  6475  tpres  6956  dfoprab2  7204  dmoprab  7247  rnoprab  7249  mpomptx  7257  resoprab  7262  elrnmpores  7280  ov3  7303  ov6g  7304  uniuni  7476  opabex3rd  7659  oprabex3  7670  wfrlem4  7950  oeeu  8221  xpassen  8603  zorn2lem6  9915  ltresr  10554  axaddf  10559  axmulf  10560  hashfun  13790  hash2prb  13822  5oalem7  29429  mpomptxf  30417  eulerpartlemgvv  31627  bnj600  32184  bnj916  32198  bnj983  32216  bnj986  32220  bnj996  32221  bnj1021  32231  dfacycgr1  32384  satfv1  32603  elima4  33012  brtxp2  33335  brpprod3a  33340  brpprod3b  33341  elfuns  33369  brcart  33386  brimg  33391  brapply  33392  brsuccf  33395  brrestrict  33403  dfrdg4  33405  ellines  33606  bj-cbvex4vv  34120  itg2addnclem3  34937  brxrn2  35619  dfxrn2  35620  ecxrn  35631  inxpxrn  35635  rnxrn  35638  dalem20  36821  dvhopellsm  38245  diblsmopel  38299  en2pr  39896  pm11.52  40709  pm11.6  40714  pm11.7  40718  opelopab4  40875  stoweidlem35  42310  fundcmpsurbijinj  43560  mpomptx2  44373