Theorem 2exbii 1849

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

Syntax hints:   ↔ wb 206  ∃wex 1779

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

This theorem depends on definitions:  df-bi 207  df-ex 1780

This theorem is referenced by:  3exbii  1850  2exanali  1860  4exdistrv  1956  3exdistr  1960  cbvex4vw  2042  eeeanv  2348  ee4anv  2349  ee4anvOLD  2350  2exsb  2358  cbvex4v  2413  2sb5rf  2470  sbel2x  2472  2mo2  2640  r3ex  3176  reeanlem  3208  rexcomf  3277  cgsex4g  3494  ceqsex3v  3503  ceqsex4v  3504  ceqsex8v  3506  copsexgw  5450  copsexg  5451  copsex2g  5453  vopelopabsb  5489  opabn0  5513  elxp2  5662  rabxp  5686  elxp3  5704  elvv  5713  elvvv  5714  copsex2gb  5769  elcnv2  5841  cnvuni  5850  cnvopab  6110  xpdifid  6141  coass  6238  fununi  6591  dfmpt3  6652  tpres  7175  dfoprab2  7447  cbvoprab3v  7481  dmoprab  7492  rnoprab  7494  mpomptx  7502  resoprab  7507  elrnmpores  7527  ov3  7552  ov6g  7553  uniuni  7738  opabex3rd  7945  oprabex3  7956  oeeu  8567  xpassen  9035  sbthfilem  9162  zorn2lem6  10454  ltresr  11093  axaddf  11098  axmulf  11099  hashfun  14402  hash2prb  14437  5oalem7  31589  mpomptxf  32601  eulerpartlemgvv  34367  bnj600  34909  bnj916  34923  bnj983  34941  bnj986  34945  bnj996  34946  bnj1021  34956  dfacycgr1  35131  satfv1  35350  elima4  35763  brtxp2  35869  brpprod3a  35874  brpprod3b  35875  elfuns  35903  brcart  35920  brimg  35925  brapply  35926  brsuccf  35929  brrestrict  35937  dfrdg4  35939  ellines  36140  bj-cbvex4vv  36793  itg2addnclem3  37667  brxrn2  38357  dfxrn2  38358  ecxrn  38373  inxpxrn  38381  rnxrn  38384  dmqsblocks  38845  dalem20  39687  dvhopellsm  41111  diblsmopel  41165  ralopabb  43400  en2pr  43536  pm11.52  44376  pm11.6  44381  pm11.7  44385  opelopab4  44541  stoweidlem35  46033  fundcmpsurbijinj  47411  mpomptx2  48323