Theorem exbidv 1921

Description: Formula-building rule for existential quantifier (deduction form). See also exbidh 1867 and exbid 2224. (Contributed by NM, 26-May-1993.)

Hypothesis

Ref	Expression
albidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
exbidv	⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem exbidv

Step	Hyp	Ref	Expression
1		ax-5 1910	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		albidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	exbidh 1867	1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Syntax hints:   → wi 4   ↔ 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  ax-5 1910

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

This theorem is referenced by:  nfbidv  1922  2exbidv  1924  3exbidv  1925  eleq1w  2811  eleq2w  2812  eleq1d  2813  eleq2dALT  2815  clelab  2873  rexbidv2  3153  rmoeq1  3384  cgsex4gOLD  3492  ceqsex2  3498  ceqsex2v  3499  alexeqg  3614  sbc2or  3759  sbc5ALT  3779  sbcex2  3811  sbcabel  3838  elpreqprlem  4826  elpreqpr  4827  eluni  4870  csbuni  4896  intab  4938  cbvopab1  5176  cbvopab1g  5177  cbvopab1s  5179  cbvopab1v  5180  axrep1  5230  axreplem  5231  zfrepclf  5241  axsepg  5247  zfauscl  5248  sels  5393  euotd  5468  opeliunxp  5698  opeliun2xp  5699  brcog  5820  elrn2g  5844  dfdmf  5850  eldmg  5852  dmopabelb  5870  dmopab2rex  5871  dfrnf  5903  elrnmpt1  5913  brcodir  6080  dfco2a  6207  cores  6210  sbcfung  6524  brprcneu  6830  brprcneuALT  6831  ssimaexg  6929  dmfco  6939  fndmdif  6996  fmptco  7083  fliftf  7272  imaeqsexvOLD  7320  oprabbidv  7435  cbvoprab1  7456  cbvoprab2  7457  cbvoprab12v  7459  imaeqexov  7607  uniuni  7718  dmtpos  8194  frecseq123  8238  csbfrecsg  8240  frrlem1  8242  frrlem13  8254  rdglim2  8377  ecdmn0  8700  mapsnd  8836  breng  8904  brdom2g  8906  domeng  8911  mapsnend  8984  isinf  9183  isinfOLD  9184  ac6sfi  9207  ordiso  9445  brwdom  9496  brwdom2  9502  zfregcl  9523  inf0  9550  zfinf  9568  ttrcleq  9638  brttrcl  9642  brttrcl2  9643  ssttrcl  9644  ttrcltr  9645  ttrclss  9649  ttrclselem2  9655  bnd2  9822  isinffi  9921  acneq  9972  acni  9974  aceq0  10047  aceq3lem  10049  dfac3  10050  dfac5lem4  10055  dfac5lem4OLD  10057  dfac8  10065  dfac9  10066  kmlem1  10080  kmlem2  10081  kmlem8  10087  kmlem10  10089  kmlem13  10092  cfval  10176  cardcf  10181  cfeq0  10185  cfsuc  10186  cff1  10187  cflim3  10191  cofsmo  10198  isfin4  10226  axcc2lem  10365  axcc4dom  10370  domtriomlem  10371  dcomex  10376  axdc2lem  10377  axdc4lem  10384  zfac  10389  ac7g  10403  ac4c  10405  ac5  10406  ac6sg  10417  weth  10424  axrepndlem1  10521  axunndlem1  10524  zfcndrep  10543  zfcndinf  10547  zfcndac  10548  gruina  10747  grothomex  10758  genpass  10938  1idpr  10958  ltexprlem3  10967  ltexprlem4  10968  ltexpri  10972  reclem2pr  10977  reclem3pr  10978  recexpr  10980  infm3  12118  nnunb  12414  axdc4uz  13925  ishashinf  14404  relexpindlem  15005  sumeq1  15631  sumeq2w  15634  sumeq2ii  15635  sumeq2sdv  15645  summo  15659  fsum  15662  fsum2dlem  15712  ntrivcvgn0  15840  ntrivcvgmullem  15843  prodeq1f  15848  prodeq1  15849  prodeq2w  15852  prodeq2ii  15853  prodeq2sdv  15865  prodmo  15878  zprod  15879  fprod  15883  fprodntriv  15884  fprod2dlem  15922  vdwapun  16921  vdwmc  16925  vdwmc2  16926  isacs  17592  dfiso2  17714  brssc  17756  isssc  17762  equivestrcsetc  18093  dirge  18544  gsumvalx  18585  gsumpropd  18587  gsumpropd2lem  18588  gsumress  18591  gsumval3eu  19818  gsumval3lem2  19820  dprd2d2  19960  znleval  21496  neitr  23100  cmpcovf  23311  hausmapdom  23420  ptval  23490  elpt  23492  ptpjopn  23532  ptclsg  23535  ptcnp  23542  uffix2  23844  cnextf  23986  prdsxmslem2  24450  metustfbas  24478  metcld2  25240  dchrmusumlema  27437  dchrisum0lema  27458  elold  27818  lrrecfr  27890  istrkgld  28439  uvtx01vtx  29377  1loopgrvd2  29484  wspthsn  29828  iswspthn  29829  wspthsnon  29832  iswspthsnon  29836  wspthnon  29838  wlkiswwlks2  29855  wlkiswwlksupgr2  29857  wlklnwwlkln2lem  29862  wlksnwwlknvbij  29888  wspthsnwspthsnon  29896  elwwlks2on  29939  elwwlks2  29946  elwspths2spth  29947  clwlkclwwlk  29981  clwwlkvbij  30092  isgrpo  30476  adjeu  31868  iunrnmptss  32544  fcoinvbr  32584  2ndresdju  32623  fmptcof2  32631  acunirnmpt  32633  acunirnmpt2  32634  acunirnmpt2f  32635  aciunf1  32637  fnpreimac  32645  fpwrelmapffslem  32705  gsumwrd2dccatlem  33049  1arithidomlem1  33499  1arithidom  33501  fmcncfil  33914  bnj865  34906  bnj1388  35016  bnj1489  35039  fineqvrep  35078  fineqvac  35080  satfrnmapom  35350  satf0op  35357  dmopab3rexdif  35385  prv1n  35411  rexxfr3dALT  35619  eldm3  35741  opelco3  35755  elsingles  35899  funpartlem  35923  dfrdg4  35932  linedegen  36124  prodeq12sdv  36199  cbvoprab2vw  36219  cbvoprab13vw  36222  cbvmodavw  36231  cbvopab1davw  36245  cbvopab2davw  36246  cbvoprab2davw  36253  cbvoprab12davw  36256  cbvoprab23davw  36257  cbvoprab13davw  36258  cbvsumdavw  36260  cbvproddavw  36261  cbvsumdavw2  36276  cbvproddavw2  36277  finminlem  36299  filnetlem4  36362  mobidvALT  36838  bj-issetwt  36856  bj-restuni  37078  bj-finsumval0  37266  csboprabg  37311  topdifinffinlem  37328  cbveud  37353  wl-sb8eut  37559  wl-sb8eutv  37560  sdclem1  37730  fdc  37732  ismgmOLD  37837  isriscg  37971  elrnres  38253  eldm4  38256  exan3  38275  exanres  38276  eldmcnv  38320  brxrn  38349  cosseq  38410  brcoss  38415  brcoss3  38417  eldm1cossres  38444  brcosscnv  38456  islshpat  39003  lshpsmreu  39095  isopos  39166  islpln5  39522  islvol5  39566  pmapjat1  39840  dibelval3  41134  diblsmopel  41158  mapdpglem3  41662  hdmapglem7a  41914  19.9dev  42195  fimgmcyc  42515  dfac11  43044  nnoeomeqom  43294  clcnvlem  43605  dfhe3  43757  ntrneineine0lem  44065  iotasbc  44401  iotasbc2  44402  brpermmodel  44986  permaxinf2lem  44995  permac8prim  44997  nregmodel  45000  fnchoice  45016  axccdom  45209  axccd  45216  stoweidlem35  46026  stoweidlem39  46030  dfatdmfcoafv2  47248  dfatco  47250  ichexmpl1  47463  ichnreuop  47466  ichreuopeq  47467  elsprel  47469  isgrim  47875  dfgric2  47908  gricushgr  47910  gricuspgr  47911  ushggricedg  47920  isubgrgrim  47922  uhgrimisgrgric  47924  grtri  47932  grtriprop  47933  isgrtri  47935  uspgrlim  47984  grlimgrtri  47988  dfgrlic2  47993  dfgrlic3  47995  grilcbri2  47996  map0cor  48836  nelsubc3lem  49052  thinccic  49453  istermc  49456  termcpropd  49485  discsntermlem  49552  basrestermcfolem  49553  discsnterm  49556  cnelsubclem  49585  bnd2d  49663