Theorem 2exbii 1944

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

Syntax hints:   ↔ wb 197  ∃wex 1874

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

This theorem depends on definitions:  df-bi 198  df-ex 1875

This theorem is referenced by:  3exbii  1945  3exdistr  2054  eeeanv  2347  ee4anv  2348  cbvex4v  2388  2sb5rf  2543  sbel2x  2551  2exsb  2562  2mo2  2672  rexcomf  3244  reean  3253  ceqsex3v  3399  ceqsex4v  3400  ceqsex8v  3402  vtocl3  3414  copsexg  5113  opelopabsbALT  5147  opabn0  5169  elxp2  5303  rabxp  5324  elxp3  5339  elvv  5347  elvvv  5348  copsex2gb  5400  elcnv2  5470  cnvuni  5479  xpdifid  5747  coass  5842  fununi  6144  dfmpt3  6194  tpres  6661  dfoprab2  6901  dmoprab  6941  rnoprab  6943  mpt2mptx  6951  resoprab  6956  elrnmpt2res  6974  ov3  6997  ov6g  6998  uniuni  7171  oprabex3  7357  wfrlem4  7623  wfrlem4OLD  7624  oeeu  7890  xpassen  8263  zorn2lem6  9578  ltresr  10216  axaddf  10221  axmulf  10222  hashfun  13428  hash2prb  13458  5oalem7  28978  mpt2mptxf  29929  eulerpartlemgvv  30888  bnj600  31440  bnj916  31454  bnj983  31472  bnj986  31475  bnj996  31476  bnj1021  31485  elima4  32125  brtxp2  32435  brpprod3a  32440  brpprod3b  32441  elfuns  32469  brcart  32486  brimg  32491  brapply  32492  brsuccf  32495  brrestrict  32503  dfrdg4  32505  ellines  32706  bj-cbvex4vv  33180  cnfinltrel  33677  itg2addnclem3  33889  brxrn2  34569  dfxrn2  34570  ecxrn  34581  inxpxrn  34585  rnxrn  34588  dalem20  35652  dvhopellsm  37076  diblsmopel  37130  pm11.52  39263  2exanali  39264  pm11.6  39269  pm11.7  39273  opelopab4  39432  stoweidlem35  40892  mpt2mptx2  42785