Theorem exbii 1658

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

This proof depends on syntax axioms:   ↔ wb 105  ∃wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-ial 1587

This proof depends on definitions:  df-bi 117

This theorem is used by:  2exbii  1659  3exbii  1660  exancom  1661  excom13  1741  exrot4  1743  eeor  1747  sbcof2  1863  sbequ8  1900  sbidm  1904  sborv  1945  19.41vv  1959  19.41vvv  1960  19.41vvvv  1961  exdistr  1965  19.42vvv  1968  exdistr2  1970  3exdistr  1971  4exdistr  1972  eean  1991  eeeanv  1993  ee4anv  1994  2sb5  2043  2sb5rf  2049  sbel2x  2058  sbexyz  2063  sbex  2064  exsb  2068  2exsb  2069  sb8eu  2099  sb8euh  2109  eu1  2111  eu2  2131  2moswapdc  2177  2exeu  2179  exists1  2183  clelab  2366  clabel  2367  sbabel  2419  rexbii2  2561  r2exf  2568  nfrexdya  2586  r19.41  2706  r19.43  2709  cbvreuvw  2792  isset  2828  rexv  2840  ceqsex2  2863  ceqsex3v  2865  gencbvex  2869  ceqsrexv  2956  rexab  2988  rexrab2  2993  euxfrdc  3012  euind  3013  reu6  3015  reu3  3016  2reuswapdc  3030  reuind  3031  sbccomlem  3126  rmo2ilem  3142  rexun  3409  reupick3  3518  abn0r  3546  abn0m  3547  rabn0m  3549  rexsns  3748  exsnrex  3751  snprc  3774  euabsn2  3780  reusn  3782  eusn  3785  snmb  3834  elunirab  3948  unipr  3949  uniun  3954  uniin  3955  iuncom4  4019  dfiun2g  4044  iunn0m  4073  iunxiun  4094  disjnim  4120  cbvopab2  4205  cbvopab2v  4208  unopab  4210  zfnuleu  4257  0ex  4260  vnex  4264  inex1  4267  intexabim  4288  iinexgm  4290  inuni  4291  unidif0  4304  axpweq  4308  zfpow  4312  axpow2  4313  axpow3  4314  vpwex  4316  zfpair2  4347  mss  4366  exss  4367  opm  4374  eqvinop  4383  copsexg  4384  opabm  4423  iunopab  4424  zfun  4579  uniex2  4581  uniex2OLD  4582  uniuni  4597  rexxfrd  4609  dtruex  4706  zfinf2  4736  elxp2  4792  opeliunxp  4830  xpiundi  4833  xpiundir  4834  elvvv  4838  eliunxp  4919  rexiunxp  4922  relop  4930  elco  4946  opelco2g  4948  cnvco  4965  cnvuni  4966  dfdm3  4967  dfrn2  4968  dfrn3  4969  elrng  4971  dfdm4  4973  eldm2g  4977  dmun  4988  dmin  4989  dmiun  4990  dmuni  4991  dmopab  4992  dmi  4996  reldmm  5000  dmmrnm  5001  elrn  5025  rnopab  5029  dmcosseq  5054  dmres  5084  elres  5099  elsnres  5100  dfima2  5128  elima3  5133  imadmrn  5136  imai  5143  args  5156  rniun  5198  ssrnres  5230  dmsnm  5253  dmsnopg  5259  elxp4  5275  elxp5  5276  cnvresima  5277  mptpreima  5281  dfco2  5287  coundi  5289  coundir  5290  resco  5292  imaco  5293  rnco  5294  coiun  5297  coi1  5303  coass  5306  xpcom  5334  dffun2  5387  imadif  5461  imainlem  5462  funimaexglem  5464  fun11iun  5660  f11o  5673  brprcneu  5688  nfvres  5732  fndmin  5816  abrexco  5965  imaiun  5966  dfoprab2  6135  cbvoprab2  6161  rexrnmpo  6204  opabex3d  6350  opabex3  6351  abexssex  6354  abexex  6355  oprabrexex2  6363  uchoice  6371  releldm2  6419  dfopab2  6423  dfoprab3s  6424  cnvoprab  6470  cnvimadfsn  6485  brtpos2  6522  tfr1onlemaccex  6619  tfrcllembxssdm  6627  tfrcllemaccex  6632  domen  7035  mapsnen  7100  xpsnen  7119  xpcomco  7124  xpassen  7128  fimax2gtri  7206  supelti  7342  cc1  7631  subhalfnqq  7781  ltbtwnnq  7783  prnmaxl  7855  prnminu  7856  prarloc  7870  genpdflem  7874  genpassl  7891  genpassu  7892  ltexprlemm  7967  2rexuz  9982  seq3f1olemp  10952  cbvsum  12126  cbvprod  12325  nnwosdc  12816  4sqlem12  13181  inffinp1  13320  ctiunctal  13332  unct  13333  isbasis2g  15146  tgval2  15152  ntreq0  15233  lmff  15350  metrest  15607  upgrex  16344  1loopgrvd2fi  16546  bj-axempty  16919  bj-axempty2  16920  bj-vprc  16922  bdinex1  16925  bj-zfpair2  16936  bj-uniex2  16942  bj-d0clsepcl  16951  wexmiddifxylem  17045  alsbii  17141