Theorem 2exbii 1868

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

Syntax hints:   ↔ wb 208  ∃wex 1798

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

This theorem depends on definitions:  df-bi 209  df-ex 1799

This theorem is referenced by:  3exbii  1869  2exanali  1879  4exdistrv  1975  3exdistr  1979  cbvex4vw  2061  eeeanv  2380  ee4anv  2381  ee4anvOLD  2382  2exsb  2390  cbvex4v  2445  2sb5rf  2502  sbel2x  2504  2mo2  2673  r3ex  3200  reeanlem  3232  rexcomf  3300  cgsex4g  3499  ceqsex3v  3505  ceqsex4v  3506  ceqsex8v  3508  copsexgw  5457  copsexgwOLD  5458  copsexg  5459  copsex2g  5461  vopelopabsb  5498  opabn0  5522  elxp2  5669  rabxp  5693  elxp3  5711  elvv  5720  elvvv  5721  copsex2gb  5777  elcnv2  5847  cnvuni  5860  cnvopab  6121  xpdifid  6150  coass  6249  fununi  6592  dfmpt3  6651  tpres  7181  dfoprab2  7450  cbvoprab3v  7484  dmoprab  7495  rnoprab  7497  mpomptx  7505  resoprab  7510  elrnmpores  7530  ov3  7555  ov6g  7556  uniuni  7741  opabex3rd  7943  oprabex3  7954  oeeu  8568  xpassen  9039  sbthfilem  9162  zorn2lem6  10455  ltresr  11095  axaddf  11100  axmulf  11101  hashfun  14447  hash2prb  14482  5oalem7  31809  mpomptxf  32830  eulerpartlemgvv  34634  bnj600  35178  bnj916  35192  bnj983  35210  bnj986  35214  bnj996  35215  bnj1021  35225  dfacycgr1  35458  satfv1  35677  elima4  36090  brtxp2  36193  brpprod3a  36198  brpprod3b  36199  elfuns  36227  brcart  36244  brimg  36249  brapply  36250  lemsuccf  36253  brrestrict  36263  dfrdg4  36265  ellines  36466  bj-cbvex4vv  37254  copsex2gd  37594  itg2addnclem3  38136  brxrn2  38847  dfxrn2  38848  ecxrn  38869  inxpxrn  38881  rnxrn  38884  dmqsblocks  39430  dalem20  40281  dvhopellsm  41705  diblsmopel  41759  ralopabb  43951  en2pr  44087  pm11.52  44927  pm11.6  44932  pm11.7  44936  opelopab4  45091  stoweidlem35  46573  fundcmpsurbijinj  47980  mpomptx2  48921