Theorem 2exbii 1879

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

This proof depends on syntax axioms:   ↔ wb 209  ∃wex 1809

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839

This proof depends on definitions:  df-bi 210  df-ex 1810

This theorem is used by:  3exbii  1880  2exanali  1890  4exdistrv  1986  3exdistr  1990  cbvex4vw  2072  eeeanv  2382  ee4anv  2383  ee4anvOLD  2384  2exsb  2392  cbvex4v  2447  2sb5rf  2504  sbel2x  2506  2mo2  2675  r3ex  3204  reeanlem  3236  rexcomf  3304  cgsex4g  3501  ceqsex3v  3507  ceqsex4v  3508  ceqsex8v  3510  copsexgw  5472  copsexgwOLD  5473  copsexg  5474  copsex2g  5476  vopelopabsb  5513  opabn0  5538  elxp2  5685  rabxp  5709  elxp3  5727  elvv  5736  elvvv  5737  copsex2gb  5793  elcnv2  5863  cnvuni  5876  cnvopab  6137  xpdifid  6165  xpdifcnvepel  6166  coass  6267  fununi  6611  dfmpt3  6669  tpres  7199  dfoprab2  7468  cbvoprab3v  7502  dmoprab  7513  rnoprab  7515  mpomptx  7523  resoprab  7528  elrnmpores  7548  ov3  7573  ov6g  7574  uniuni  7757  opabex3rd  7959  oprabex3  7970  oeeu  8585  xpassen  9055  sbthfilem  9178  zorn2lem6  10489  ltresr  11129  axaddf  11134  axmulf  11135  hashfun  14479  hash2prb  14514  5oalem7  32021  mpomptxf  33032  eulerpartlemgvv  34775  bnj600  35316  bnj916  35330  bnj983  35348  bnj986  35352  bnj996  35353  bnj1021  35363  dfacycgr1  35644  satfv1  35863  elima4  36276  brtxp2  36379  brpprod3a  36384  brpprod3b  36385  elfuns  36413  brcart  36430  brimg  36435  brapply  36436  lemsuccf  36439  brrestrict  36449  dfrdg4  36451  ellines  36652  bj-cbvex4vv  37468  copsex2gd  37810  itg2addnclem3  38352  brxrn2  39061  dfxrn2  39062  ecxrn  39083  inxpxrn  39095  rnxrn  39098  dmqsblocks  39644  dalem20  40495  dvhopellsm  41919  diblsmopel  41973  ralopabb  44165  en2pr  44301  pm11.52  45125  pm11.6  45130  pm11.7  45134  opelopab4  45288  stoweidlem35  46777  fundcmpsurbijinj  48187  mpomptx2  49143