Theorem 2exbii 1948

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

Syntax hints:   ↔ wb 198  ∃wex 1878

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

This theorem depends on definitions:  df-bi 199  df-ex 1879

This theorem is referenced by:  3exbii  1949  4exdistrv  2055  3exdistr  2059  eeeanv  2374  ee4anv  2375  2exsb  2383  cbvex4v  2435  2sb5rf  2585  sbel2x  2592  2mo2  2730  rexcomf  3307  reean  3316  ceqsex3v  3463  ceqsex4v  3464  ceqsex8v  3466  vtocl3  3478  copsexg  5178  opelopabsbALT  5212  opabn0  5234  elxp2  5370  rabxp  5391  elxp3  5406  elvv  5414  elvvv  5415  copsex2gb  5468  elcnv2  5536  cnvuni  5545  xpdifid  5807  coass  5899  fununi  6201  dfmpt3  6251  tpres  6727  dfoprab2  6966  dmoprab  7006  rnoprab  7008  mpt2mptx  7016  resoprab  7021  elrnmpt2res  7039  ov3  7062  ov6g  7063  uniuni  7236  oprabex3  7422  wfrlem4  7688  wfrlem4OLD  7689  oeeu  7955  xpassen  8329  zorn2lem6  9645  ltresr  10284  axaddf  10289  axmulf  10290  hashfun  13520  hash2prb  13550  5oalem7  29070  mpt2mptxf  30021  eulerpartlemgvv  30979  bnj600  31531  bnj916  31545  bnj983  31563  bnj986  31566  bnj996  31567  bnj1021  31576  elima4  32212  brtxp2  32522  brpprod3a  32527  brpprod3b  32528  elfuns  32556  brcart  32573  brimg  32578  brapply  32579  brsuccf  32582  brrestrict  32590  dfrdg4  32592  ellines  32793  bj-cbvex4vv  33273  cnfinltrel  33781  itg2addnclem3  34001  brxrn2  34680  dfxrn2  34681  ecxrn  34692  inxpxrn  34696  rnxrn  34699  dalem20  35763  dvhopellsm  37187  diblsmopel  37241  pm11.52  39421  2exanali  39422  pm11.6  39427  pm11.7  39431  opelopab4  39590  stoweidlem35  41040  mpt2mptx2  42974