Theorem 2exbii 1881

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

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

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

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

This theorem is used by:  3exbii  1882  2exanali  1892  4exdistrv  1988  3exdistr  1992  cbvex4vw  2074  eeeanv  2379  ee4anv  2380  ee4anvOLD  2381  2exsb  2389  cbvex4v  2444  2sb5rf  2501  sbel2x  2503  2mo2  2672  r3ex  3201  reeanlem  3233  rexcomf  3301  cgsex4g  3496  ceqsex3v  3502  ceqsex4v  3503  ceqsex8v  3505  copsexgw  5459  copsexgwOLD  5460  copsexg  5461  copsex2g  5464  vopelopabsb  5502  opabn0  5527  elxp2  5674  rabxp  5698  elxp3  5716  elvv  5725  elvvv  5726  copsex2gb  5783  elcnv2  5854  cnvuni  5867  cnvopab  6130  xpdifid  6158  xpdifcnvepel  6159  coass  6267  fununi  6615  dfmpt3  6673  tpres  7207  dfoprab2  7478  cbvoprab3v  7512  dmoprab  7523  rnoprab  7525  mpomptx  7533  resoprab  7538  elrnmpores  7558  ov3  7583  ov6g  7584  uniuni  7776  opabex3rd  7978  oprabex3  7989  oeeu  8615  xpassen  9093  sbthfilem  9216  zorn2lem6  10582  ltresr  11228  axaddf  11233  axmulf  11234  hashfun  14585  hash2prb  14620  degenmgm2nfun  19144  dfric2  20762  dfacycgr1  30755  5oalem7  32267  mpomptxf  33319  eulerpartlemgvv  35054  bnj600  35595  bnj916  35609  bnj983  35627  bnj986  35631  bnj996  35632  bnj1021  35642  satfv1  36214  elima4  36632  brtxp2  36735  brpprod3a  36740  brpprod3b  36741  elfuns  36769  brcart  36786  brimg  36791  brapply  36792  lemsuccf  36795  brrestrict  36805  dfrdg4  36807  ellines  37009  bj-cbvex4vv  37809  copsex2gd  38152  itg2addnclem3  38684  brxrn2  39409  dfxrn2  39410  ecxrn  39431  inxpxrn  39443  rnxrn  39446  dmqsblocks  39992  dalem20  40843  dvhopellsm  42267  diblsmopel  42321  ralopabb  44505  en2pr  44641  pm11.52  45464  pm11.6  45469  pm11.7  45473  opelopab4  45627  stoweidlem35  47138  fundcmpsurbijinj  48585  mpomptx2  49540