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  2381  ee4anv  2382  ee4anvOLD  2383  2exsb  2391  cbvex4v  2446  2sb5rf  2503  sbel2x  2505  2mo2  2674  r3ex  3203  reeanlem  3235  rexcomf  3303  cgsex4g  3499  ceqsex3v  3505  ceqsex4v  3506  ceqsex8v  3508  copsexgw  5470  copsexgwOLD  5471  copsexg  5472  copsex2g  5474  vopelopabsb  5511  opabn0  5536  elxp2  5683  rabxp  5707  elxp3  5725  elvv  5734  elvvv  5735  copsex2gb  5791  elcnv2  5861  cnvuni  5874  cnvopab  6135  xpdifid  6164  xpdifcnvepel  6165  coass  6266  fununi  6612  dfmpt3  6670  tpres  7204  dfoprab2  7475  cbvoprab3v  7509  dmoprab  7520  rnoprab  7522  mpomptx  7530  resoprab  7535  elrnmpores  7555  ov3  7580  ov6g  7581  uniuni  7765  opabex3rd  7967  oprabex3  7978  oeeu  8595  xpassen  9073  sbthfilem  9196  zorn2lem6  10507  ltresr  11153  axaddf  11158  axmulf  11159  hashfun  14506  hash2prb  14541  degenmgm2nfun  19058  dfacycgr1  30637  5oalem7  32149  mpomptxf  33159  eulerpartlemgvv  34895  bnj600  35436  bnj916  35450  bnj983  35468  bnj986  35472  bnj996  35473  bnj1021  35483  satfv1  35950  elima4  36363  brtxp2  36466  brpprod3a  36471  brpprod3b  36472  elfuns  36500  brcart  36517  brimg  36522  brapply  36523  lemsuccf  36526  brrestrict  36536  dfrdg4  36538  ellines  36740  bj-cbvex4vv  37556  copsex2gd  37898  itg2addnclem3  38430  brxrn2  39140  dfxrn2  39141  ecxrn  39162  inxpxrn  39174  rnxrn  39177  dmqsblocks  39723  dalem20  40574  dvhopellsm  41998  diblsmopel  42052  ralopabb  44259  en2pr  44395  pm11.52  45219  pm11.6  45224  pm11.7  45228  opelopab4  45382  stoweidlem35  46871  fundcmpsurbijinj  48318  mpomptx2  49273