Theorem 2exbii 1856

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

Syntax hints:   ↔ wb 207  ∃wex 1786

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

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  3exbii  1857  2exanali  1867  4exdistrv  1963  3exdistr  1967  cbvex4vw  2049  eeeanv  2358  ee4anv  2359  ee4anvOLD  2360  2exsb  2368  cbvex4v  2423  2sb5rf  2480  sbel2x  2482  2mo2  2651  r3ex  3179  reeanlem  3211  rexcomf  3279  cgsex4g  3479  ceqsex3v  3486  ceqsex4v  3487  ceqsex8v  3489  copsexgw  5437  copsexgwOLD  5438  copsexg  5439  copsex2g  5441  vopelopabsb  5478  opabn0  5502  elxp2  5649  rabxp  5673  elxp3  5691  elvv  5700  elvvv  5701  copsex2gb  5756  elcnv2  5826  cnvuni  5835  cnvopab  6094  xpdifid  6126  coass  6224  fununi  6567  dfmpt3  6626  tpres  7152  dfoprab2  7421  cbvoprab3v  7455  dmoprab  7466  rnoprab  7468  mpomptx  7476  resoprab  7481  elrnmpores  7501  ov3  7526  ov6g  7527  uniuni  7712  opabex3rd  7915  oprabex3  7926  oeeu  8536  xpassen  9006  sbthfilem  9129  zorn2lem6  10421  ltresr  11061  axaddf  11066  axmulf  11067  hashfun  14397  hash2prb  14432  5oalem7  31756  mpomptxf  32777  eulerpartlemgvv  34567  bnj600  35108  bnj916  35122  bnj983  35140  bnj986  35144  bnj996  35145  bnj1021  35155  dfacycgr1  35379  satfv1  35598  elima4  36011  brtxp2  36114  brpprod3a  36119  brpprod3b  36120  elfuns  36148  brcart  36165  brimg  36170  brapply  36171  lemsuccf  36174  brrestrict  36184  dfrdg4  36186  ellines  36387  bj-cbvex4vv  37165  copsex2gd  37505  itg2addnclem3  38047  brxrn2  38758  dfxrn2  38759  ecxrn  38780  inxpxrn  38792  rnxrn  38795  dmqsblocks  39341  dalem20  40192  dvhopellsm  41616  diblsmopel  41670  ralopabb  43862  en2pr  43998  pm11.52  44838  pm11.6  44843  pm11.7  44847  opelopab4  45002  stoweidlem35  46485  fundcmpsurbijinj  47892  mpomptx2  48833