Theorem 2exbii 1852

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

Syntax hints:   ↔ wb 205  ∃wex 1782

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

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  3exbii  1853  2exanali  1864  4exdistrv  1961  3exdistr  1965  cbvex4vw  2046  eeeanv  2349  ee4anv  2350  2exsb  2359  cbvex4v  2416  2sb5rf  2473  sbel2x  2475  2mo2  2650  rexcomf  3285  reeanlem  3293  ceqsex3v  3485  ceqsex4v  3486  ceqsex8v  3488  copsexgw  5405  copsexg  5406  copsex2g  5408  vopelopabsb  5443  opabn0  5467  elxp2  5614  rabxp  5636  elxp3  5654  elvv  5662  elvvv  5663  copsex2gb  5718  elcnv2  5789  cnvuni  5798  xpdifid  6076  coass  6173  fununi  6516  dfmpt3  6576  tpres  7085  dfoprab2  7342  dmoprab  7385  rnoprab  7387  mpomptx  7396  resoprab  7401  elrnmpores  7420  ov3  7444  ov6g  7445  uniuni  7621  opabex3rd  7818  oprabex3  7829  wfrlem4OLD  8152  oeeu  8443  xpassen  8862  sbthfilem  8993  zorn2lem6  10266  ltresr  10905  axaddf  10910  axmulf  10911  hashfun  14161  hash2prb  14195  5oalem7  30031  mpomptxf  31025  eulerpartlemgvv  32352  bnj600  32908  bnj916  32922  bnj983  32940  bnj986  32944  bnj996  32945  bnj1021  32955  dfacycgr1  33115  satfv1  33334  elima4  33759  brtxp2  34192  brpprod3a  34197  brpprod3b  34198  elfuns  34226  brcart  34243  brimg  34248  brapply  34249  brsuccf  34252  brrestrict  34260  dfrdg4  34262  ellines  34463  bj-cbvex4vv  34996  itg2addnclem3  35839  brxrn2  36512  dfxrn2  36513  ecxrn  36524  inxpxrn  36528  rnxrn  36531  dalem20  37714  dvhopellsm  39138  diblsmopel  39192  en2pr  41161  pm11.52  42012  pm11.6  42017  pm11.7  42021  opelopab4  42178  stoweidlem35  43583  fundcmpsurbijinj  44873  mpomptx2  45681