Theorem 2exbii 1844

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

Syntax hints:   ↔ wb 205  ∃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 206  df-ex 1775

This theorem is referenced by:  3exbii  1845  2exanali  1856  4exdistrv  1953  3exdistr  1957  cbvex4vw  2038  eeeanv  2341  ee4anv  2342  2exsb  2351  cbvex4v  2409  2sb5rf  2466  sbel2x  2468  2mo2  2636  reeanlem  3216  rexcomf  3291  cgsex4g  3511  ceqsex3v  3523  ceqsex4v  3524  ceqsex8v  3526  copsexgw  5496  copsexg  5497  copsex2g  5499  vopelopabsb  5535  opabn0  5559  elxp2  5706  rabxp  5730  elxp3  5748  elvv  5756  elvvv  5757  copsex2gb  5812  elcnv2  5884  cnvuni  5893  cnvopab  6149  xpdifid  6179  coass  6276  fununi  6634  dfmpt3  6695  tpres  7218  dfoprab2  7483  dmoprab  7527  rnoprab  7529  mpomptx  7538  resoprab  7543  elrnmpores  7564  ov3  7589  ov6g  7590  uniuni  7770  opabex3rd  7980  oprabex3  7991  wfrlem4OLD  8342  oeeu  8633  xpassen  9104  sbthfilem  9235  zorn2lem6  10544  ltresr  11183  axaddf  11188  axmulf  11189  hashfun  14454  hash2prb  14491  5oalem7  31593  mpomptxf  32595  eulerpartlemgvv  34210  bnj600  34764  bnj916  34778  bnj983  34796  bnj986  34800  bnj996  34801  bnj1021  34811  dfacycgr1  34972  satfv1  35191  elima4  35599  brtxp2  35705  brpprod3a  35710  brpprod3b  35711  elfuns  35739  brcart  35756  brimg  35761  brapply  35762  brsuccf  35765  brrestrict  35773  dfrdg4  35775  ellines  35976  bj-cbvex4vv  36510  itg2addnclem3  37374  brxrn2  38073  dfxrn2  38074  ecxrn  38085  inxpxrn  38093  rnxrn  38096  dalem20  39392  dvhopellsm  40816  diblsmopel  40870  ralopabb  43078  en2pr  43214  pm11.52  44061  pm11.6  44066  pm11.7  44070  opelopab4  44227  stoweidlem35  45656  fundcmpsurbijinj  46982  mpomptx2  47713