Theorem exbii 1629

Description: Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.)

Hypothesis

Ref	Expression
exbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
exbii	⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓)

Proof of Theorem exbii

Step	Hyp	Ref	Expression
1		exbi 1628	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
2		exbii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpg 1475	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓)

Syntax hints:   ↔ wb 105  ∃wex 1516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-ial 1558

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2exbii  1630  3exbii  1631  exancom  1632  excom13  1713  exrot4  1715  eeor  1719  sbcof2  1834  sbequ8  1871  sbidm  1875  sborv  1915  19.41vv  1928  19.41vvv  1929  19.41vvvv  1930  exdistr  1934  19.42vvv  1937  exdistr2  1939  3exdistr  1940  4exdistr  1941  eean  1960  eeeanv  1962  ee4anv  1963  2sb5  2012  2sb5rf  2018  sbel2x  2027  sbexyz  2032  sbex  2033  exsb  2037  2exsb  2038  sb8eu  2068  sb8euh  2078  eu1  2080  eu2  2099  2moswapdc  2145  2exeu  2147  exists1  2151  clelab  2332  clabel  2333  sbabel  2376  rexbii2  2518  r2exf  2525  nfrexdya  2543  r19.41  2662  r19.43  2665  cbvreuvw  2745  isset  2780  rexv  2792  ceqsex2  2815  ceqsex3v  2817  gencbvex  2821  ceqsrexv  2907  rexab  2939  rexrab2  2944  euxfrdc  2963  euind  2964  reu6  2966  reu3  2967  2reuswapdc  2981  reuind  2982  sbccomlem  3077  rmo2ilem  3092  rexun  3357  reupick3  3462  abn0r  3489  abn0m  3490  rabn0m  3492  rexsns  3677  exsnrex  3680  snprc  3703  euabsn2  3707  reusn  3709  eusn  3712  snmb  3759  elunirab  3869  unipr  3870  uniun  3875  uniin  3876  iuncom4  3940  dfiun2g  3965  iunn0m  3994  iunxiun  4015  disjnim  4041  cbvopab2  4126  cbvopab2v  4129  unopab  4131  zfnuleu  4176  0ex  4179  vnex  4183  inex1  4186  intexabim  4204  iinexgm  4206  inuni  4207  unidif0  4219  axpweq  4223  zfpow  4227  axpow2  4228  axpow3  4229  vpwex  4231  zfpair2  4262  mss  4278  exss  4279  opm  4286  eqvinop  4295  copsexg  4296  opabm  4335  iunopab  4336  zfun  4489  uniex2  4491  uniuni  4506  rexxfrd  4518  dtruex  4615  zfinf2  4645  elxp2  4701  opeliunxp  4738  xpiundi  4741  xpiundir  4742  elvvv  4746  eliunxp  4825  rexiunxp  4828  relop  4836  elco  4852  opelco2g  4854  cnvco  4871  cnvuni  4872  dfdm3  4873  dfrn2  4874  dfrn3  4875  elrng  4877  dfdm4  4879  eldm2g  4883  dmun  4894  dmin  4895  dmiun  4896  dmuni  4897  dmopab  4898  dmi  4902  dmmrnm  4906  elrn  4930  rnopab  4934  dmcosseq  4959  dmres  4989  elres  5004  elsnres  5005  dfima2  5033  elima3  5038  imadmrn  5041  imai  5047  args  5060  rniun  5102  ssrnres  5134  dmsnm  5157  dmsnopg  5163  elxp4  5179  elxp5  5180  cnvresima  5181  mptpreima  5185  dfco2  5191  coundi  5193  coundir  5194  resco  5196  imaco  5197  rnco  5198  coiun  5201  coi1  5207  coass  5210  xpcom  5238  dffun2  5290  imadif  5363  imainlem  5364  funimaexglem  5366  fun11iun  5555  f11o  5567  brprcneu  5582  nfvres  5623  fndmin  5700  abrexco  5841  imaiun  5842  dfoprab2  6005  cbvoprab2  6031  rexrnmpo  6074  opabex3d  6219  opabex3  6220  abexssex  6223  abexex  6224  oprabrexex2  6228  uchoice  6236  releldm2  6284  dfopab2  6288  dfoprab3s  6289  cnvoprab  6333  brtpos2  6350  tfr1onlemaccex  6447  tfrcllembxssdm  6455  tfrcllemaccex  6460  domen  6853  mapsnen  6917  xpsnen  6931  xpcomco  6936  xpassen  6940  fimax2gtri  7013  supelti  7119  cc1  7397  subhalfnqq  7547  ltbtwnnq  7549  prnmaxl  7621  prnminu  7622  prarloc  7636  genpdflem  7640  genpassl  7657  genpassu  7658  ltexprlemm  7733  2rexuz  9723  seq3f1olemp  10682  cbvsum  11746  cbvprod  11944  nnwosdc  12435  4sqlem12  12800  inffinp1  12875  ctiunctal  12887  unct  12888  isbasis2g  14592  tgval2  14598  ntreq0  14679  lmff  14796  metrest  15053  upgrex  15774  bj-axempty  15967  bj-axempty2  15968  bj-vprc  15970  bdinex1  15973  bj-zfpair2  15984  bj-uniex2  15990  bj-d0clsepcl  15999