Theorem 2exbii 1882

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

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

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

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

This theorem is used by:  3exbii  1883  2exanali  1893  4exdistrv  1989  3exdistr  1993  cbvex4vw  2075  eeeanv  2385  ee4anv  2386  ee4anvOLD  2387  2exsb  2395  cbvex4v  2450  2sb5rf  2507  sbel2x  2509  2mo2  2678  r3ex  3207  reeanlem  3239  rexcomf  3307  cgsex4g  3504  ceqsex3v  3510  ceqsex4v  3511  ceqsex8v  3513  copsexgw  5477  copsexgwOLD  5478  copsexg  5479  copsex2g  5481  vopelopabsb  5518  opabn0  5543  elxp2  5690  rabxp  5714  elxp3  5732  elvv  5741  elvvv  5742  copsex2gb  5798  elcnv2  5868  cnvuni  5881  cnvopab  6142  xpdifid  6170  xpdifcnvepel  6171  coass  6272  fununi  6618  dfmpt3  6676  tpres  7206  dfoprab2  7481  cbvoprab3v  7515  dmoprab  7526  rnoprab  7528  mpomptx  7536  resoprab  7541  elrnmpores  7561  ov3  7586  ov6g  7587  uniuni  7770  opabex3rd  7972  oprabex3  7983  oeeu  8598  xpassen  9069  sbthfilem  9192  zorn2lem6  10503  ltresr  11143  axaddf  11148  axmulf  11149  hashfun  14494  hash2prb  14529  5oalem7  32049  mpomptxf  33060  eulerpartlemgvv  34798  bnj600  35339  bnj916  35353  bnj983  35371  bnj986  35375  bnj996  35376  bnj1021  35386  dfacycgr1  35657  satfv1  35876  elima4  36289  brtxp2  36392  brpprod3a  36397  brpprod3b  36398  elfuns  36426  brcart  36443  brimg  36448  brapply  36449  lemsuccf  36452  brrestrict  36462  dfrdg4  36464  ellines  36665  bj-cbvex4vv  37481  copsex2gd  37823  itg2addnclem3  38365  brxrn2  39074  dfxrn2  39075  ecxrn  39096  inxpxrn  39108  rnxrn  39111  dmqsblocks  39657  dalem20  40508  dvhopellsm  41932  diblsmopel  41986  ralopabb  44178  en2pr  44314  pm11.52  45138  pm11.6  45143  pm11.7  45147  opelopab4  45301  stoweidlem35  46790  fundcmpsurbijinj  48200  mpomptx2  49156