Theorem 2exbii 1845

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

Syntax hints:   ↔ wb 208  ∃wex 1776

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

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

This theorem is referenced by:  3exbii  1846  2exanali  1856  4exdistrv  1953  3exdistr  1958  cbvex4vw  2045  eeeanv  2367  ee4anv  2368  2exsb  2375  cbvex4v  2433  2sb5rf  2492  sbel2x  2494  2mo2  2728  rexcomOLD  3356  rexcomf  3358  reeanlem  3365  ceqsex3v  3545  ceqsex4v  3546  ceqsex8v  3548  copsexgw  5373  copsexg  5374  opelopabsbALT  5408  opabn0  5432  elxp2  5573  rabxp  5594  elxp3  5612  elvv  5620  elvvv  5621  copsex2gb  5673  elcnv2  5742  cnvuni  5751  xpdifid  6019  coass  6112  fununi  6423  dfmpt3  6476  tpres  6957  dfoprab2  7206  dmoprab  7249  rnoprab  7251  mpomptx  7259  resoprab  7264  elrnmpores  7282  ov3  7305  ov6g  7306  uniuni  7478  opabex3rd  7661  oprabex3  7672  wfrlem4  7952  oeeu  8223  xpassen  8605  zorn2lem6  9917  ltresr  10556  axaddf  10561  axmulf  10562  hashfun  13792  hash2prb  13824  5oalem7  29431  mpomptxf  30419  eulerpartlemgvv  31629  bnj600  32186  bnj916  32200  bnj983  32218  bnj986  32222  bnj996  32223  bnj1021  32233  dfacycgr1  32386  satfv1  32605  elima4  33014  brtxp2  33337  brpprod3a  33342  brpprod3b  33343  elfuns  33371  brcart  33388  brimg  33393  brapply  33394  brsuccf  33397  brrestrict  33405  dfrdg4  33407  ellines  33608  bj-cbvex4vv  34122  itg2addnclem3  34939  brxrn2  35621  dfxrn2  35622  ecxrn  35633  inxpxrn  35637  rnxrn  35640  dalem20  36823  dvhopellsm  38247  diblsmopel  38301  en2pr  39899  pm11.52  40712  pm11.6  40717  pm11.7  40721  opelopab4  40878  stoweidlem35  42314  fundcmpsurbijinj  43564  mpomptx2  44377