Theorem exbii 1619

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 1618	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
2		exbii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpg 1465	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓)

Syntax hints:   ↔ wb 105  ∃wex 1506

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-ial 1548

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2exbii  1620  3exbii  1621  exancom  1622  excom13  1703  exrot4  1705  eeor  1709  sbcof2  1824  sbequ8  1861  sbidm  1865  sborv  1905  19.41vv  1918  19.41vvv  1919  19.41vvvv  1920  exdistr  1924  19.42vvv  1927  exdistr2  1929  3exdistr  1930  4exdistr  1931  eean  1950  eeeanv  1952  ee4anv  1953  2sb5  2002  2sb5rf  2008  sbel2x  2017  sbexyz  2022  sbex  2023  exsb  2027  2exsb  2028  sb8eu  2058  sb8euh  2068  eu1  2070  eu2  2089  2moswapdc  2135  2exeu  2137  exists1  2141  clelab  2322  clabel  2323  sbabel  2366  rexbii2  2508  r2exf  2515  nfrexdya  2533  r19.41  2652  r19.43  2655  cbvreuvw  2735  isset  2769  rexv  2781  ceqsex2  2804  ceqsex3v  2806  gencbvex  2810  ceqsrexv  2894  rexab  2926  rexrab2  2931  euxfrdc  2950  euind  2951  reu6  2953  reu3  2954  2reuswapdc  2968  reuind  2969  sbccomlem  3064  rmo2ilem  3079  rexun  3344  reupick3  3449  abn0r  3476  abn0m  3477  rabn0m  3479  rexsns  3662  exsnrex  3665  snprc  3688  euabsn2  3692  reusn  3694  eusn  3697  elunirab  3853  unipr  3854  uniun  3859  uniin  3860  iuncom4  3924  dfiun2g  3949  iunn0m  3978  iunxiun  3999  disjnim  4025  cbvopab2  4108  cbvopab2v  4111  unopab  4113  zfnuleu  4158  0ex  4161  vnex  4165  inex1  4168  intexabim  4186  iinexgm  4188  inuni  4189  unidif0  4201  axpweq  4205  zfpow  4209  axpow2  4210  axpow3  4211  vpwex  4213  zfpair2  4244  mss  4260  exss  4261  opm  4268  eqvinop  4277  copsexg  4278  opabm  4316  iunopab  4317  zfun  4470  uniex2  4472  uniuni  4487  rexxfrd  4499  dtruex  4596  zfinf2  4626  elxp2  4682  opeliunxp  4719  xpiundi  4722  xpiundir  4723  elvvv  4727  eliunxp  4806  rexiunxp  4809  relop  4817  elco  4833  opelco2g  4835  cnvco  4852  cnvuni  4853  dfdm3  4854  dfrn2  4855  dfrn3  4856  elrng  4858  dfdm4  4859  eldm2g  4863  dmun  4874  dmin  4875  dmiun  4876  dmuni  4877  dmopab  4878  dmi  4882  dmmrnm  4886  elrn  4910  rnopab  4914  dmcosseq  4938  dmres  4968  elres  4983  elsnres  4984  dfima2  5012  elima3  5017  imadmrn  5020  imai  5026  args  5039  rniun  5081  ssrnres  5113  dmsnm  5136  dmsnopg  5142  elxp4  5158  elxp5  5159  cnvresima  5160  mptpreima  5164  dfco2  5170  coundi  5172  coundir  5173  resco  5175  imaco  5176  rnco  5177  coiun  5180  coi1  5186  coass  5189  xpcom  5217  dffun2  5269  imadif  5339  imainlem  5340  funimaexglem  5342  fun11iun  5528  f11o  5540  brprcneu  5554  nfvres  5595  fndmin  5672  abrexco  5809  imaiun  5810  dfoprab2  5973  cbvoprab2  5999  rexrnmpo  6042  opabex3d  6187  opabex3  6188  abexssex  6191  abexex  6192  oprabrexex2  6196  uchoice  6204  releldm2  6252  dfopab2  6256  dfoprab3s  6257  cnvoprab  6301  brtpos2  6318  tfr1onlemaccex  6415  tfrcllembxssdm  6423  tfrcllemaccex  6428  domen  6819  mapsnen  6879  xpsnen  6889  xpcomco  6894  xpassen  6898  fimax2gtri  6971  supelti  7077  cc1  7348  subhalfnqq  7498  ltbtwnnq  7500  prnmaxl  7572  prnminu  7573  prarloc  7587  genpdflem  7591  genpassl  7608  genpassu  7609  ltexprlemm  7684  2rexuz  9673  seq3f1olemp  10624  cbvsum  11542  cbvprod  11740  nnwosdc  12231  4sqlem12  12596  inffinp1  12671  ctiunctal  12683  unct  12684  isbasis2g  14365  tgval2  14371  ntreq0  14452  lmff  14569  metrest  14826  bj-axempty  15623  bj-axempty2  15624  bj-vprc  15626  bdinex1  15629  bj-zfpair2  15640  bj-uniex2  15646  bj-d0clsepcl  15655