Theorem exbidv 1920

Description: Formula-building rule for existential quantifier (deduction form). See also exbidh 1866 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 1909	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		albidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	exbidh 1866	1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 206  ∃wex 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

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

This theorem is referenced by:  nfbidv  1921  2exbidv  1923  3exbidv  1924  eleq1w  2827  eleq2w  2828  eleq1d  2829  eleq2dALT  2831  clelab  2890  rexbidv2  3181  rmoeq1  3425  cgsex4gOLD  3539  ceqsex2  3547  ceqsex2v  3548  alexeqg  3664  sbc2or  3813  sbc5ALT  3833  sbcex2  3869  sbcabel  3900  elpreqprlem  4890  elpreqpr  4891  eluni  4934  csbuni  4960  intab  5002  cbvopab1  5241  cbvopab1g  5242  cbvopab1s  5244  cbvopab1v  5245  axrep1  5304  axreplem  5305  zfrepclf  5312  axsepg  5318  zfauscl  5319  sels  5458  euotd  5532  opeliunxp  5767  brcog  5891  elrn2g  5915  dfdmf  5921  eldmg  5923  dmopabelb  5941  dmopab2rex  5942  dfrnf  5975  elrnmpt1  5983  brcodir  6151  dfco2a  6277  cores  6280  sbcfung  6602  brprcneu  6910  brprcneuALT  6911  ssimaexg  7008  dmfco  7018  fndmdif  7075  fmptco  7163  fliftf  7351  imaeqsexvOLD  7399  oprabbidv  7516  cbvoprab1  7537  cbvoprab2  7538  cbvoprab12v  7540  imaeqexov  7688  uniuni  7797  dmtpos  8279  frecseq123  8323  csbfrecsg  8325  frrlem1  8327  frrlem13  8339  wrecseq123OLD  8356  wfrlem1OLD  8364  wfrlem3OLDa  8367  wfrlem15OLD  8379  rdglim2  8488  ecdmn0  8812  mapsnd  8944  breng  9012  brenOLD  9014  brdom2g  9015  brdomgOLD  9017  domeng  9022  mapsnend  9101  isinf  9323  isinfOLD  9324  ac6sfi  9348  ordiso  9585  brwdom  9636  brwdom2  9642  zfregcl  9663  inf0  9690  zfinf  9708  ttrcleq  9778  brttrcl  9782  brttrcl2  9783  ssttrcl  9784  ttrcltr  9785  ttrclss  9789  ttrclselem2  9795  bnd2  9962  isinffi  10061  acneq  10112  acni  10114  aceq0  10187  aceq3lem  10189  dfac3  10190  dfac5lem4  10195  dfac5lem4OLD  10197  dfac8  10205  dfac9  10206  kmlem1  10220  kmlem2  10221  kmlem8  10227  kmlem10  10229  kmlem13  10232  cfval  10316  cardcf  10321  cfeq0  10325  cfsuc  10326  cff1  10327  cflim3  10331  cofsmo  10338  isfin4  10366  axcc2lem  10505  axcc4dom  10510  domtriomlem  10511  dcomex  10516  axdc2lem  10517  axdc4lem  10524  zfac  10529  ac7g  10543  ac4c  10545  ac5  10546  ac6sg  10557  weth  10564  axrepndlem1  10661  axunndlem1  10664  zfcndrep  10683  zfcndinf  10687  zfcndac  10688  gruina  10887  grothomex  10898  genpass  11078  1idpr  11098  ltexprlem3  11107  ltexprlem4  11108  ltexpri  11112  reclem2pr  11117  reclem3pr  11118  recexpr  11120  infm3  12254  nnunb  12549  axdc4uz  14035  ishashinf  14512  relexpindlem  15112  sumeq1  15737  sumeq2w  15740  sumeq2ii  15741  sumeq2sdv  15751  summo  15765  fsum  15768  fsum2dlem  15818  ntrivcvgn0  15946  ntrivcvgmullem  15949  prodeq1f  15954  prodeq1  15955  prodeq2w  15958  prodeq2ii  15959  prodeq2sdv  15971  prodmo  15984  zprod  15985  fprod  15989  fprodntriv  15990  fprod2dlem  16028  vdwapun  17021  vdwmc  17025  vdwmc2  17026  isacs  17709  dfiso2  17833  brssc  17875  isssc  17881  equivestrcsetc  18221  dirge  18673  gsumvalx  18714  gsumpropd  18716  gsumpropd2lem  18717  gsumress  18720  gsumval3eu  19946  gsumval3lem2  19948  dprd2d2  20088  znleval  21596  neitr  23209  cmpcovf  23420  hausmapdom  23529  ptval  23599  elpt  23601  ptpjopn  23641  ptclsg  23644  ptcnp  23651  uffix2  23953  cnextf  24095  prdsxmslem2  24563  metustfbas  24591  metcld2  25360  dchrmusumlema  27555  dchrisum0lema  27576  elold  27926  lrrecfr  27994  istrkgld  28485  uvtx01vtx  29432  1loopgrvd2  29539  wspthsn  29881  iswspthn  29882  wspthsnon  29885  iswspthsnon  29889  wspthnon  29891  wlkiswwlks2  29908  wlkiswwlksupgr2  29910  wlklnwwlkln2lem  29915  wlksnwwlknvbij  29941  wspthsnwspthsnon  29949  elwwlks2on  29992  elwwlks2  29999  elwspths2spth  30000  clwlkclwwlk  30034  clwwlkvbij  30145  isgrpo  30529  adjeu  31921  iunrnmptss  32588  fcoinvbr  32627  2ndresdju  32667  fmptcof2  32675  acunirnmpt  32677  acunirnmpt2  32678  acunirnmpt2f  32679  aciunf1  32681  fnpreimac  32689  fpwrelmapffslem  32746  1arithidomlem1  33528  1arithidom  33530  fmcncfil  33877  bnj865  34899  bnj1388  35009  bnj1489  35032  fineqvrep  35071  fineqvac  35073  satfrnmapom  35338  satf0op  35345  dmopab3rexdif  35373  prv1n  35399  rexxfr3dALT  35607  eldm3  35723  opelco3  35738  elsingles  35882  funpartlem  35906  dfrdg4  35915  linedegen  36107  prodeq12sdv  36184  cbvoprab2vw  36204  cbvoprab13vw  36207  cbvmodavw  36216  cbvopab1davw  36230  cbvopab2davw  36231  cbvoprab2davw  36238  cbvoprab12davw  36241  cbvoprab23davw  36242  cbvoprab13davw  36243  cbvsumdavw  36245  cbvproddavw  36246  cbvsumdavw2  36261  cbvproddavw2  36262  finminlem  36284  filnetlem4  36347  mobidvALT  36823  bj-issetwt  36841  bj-restuni  37063  bj-finsumval0  37251  csboprabg  37296  topdifinffinlem  37313  cbveud  37338  wl-sb8eut  37532  wl-sb8eutv  37533  sdclem1  37703  fdc  37705  ismgmOLD  37810  isriscg  37944  elrnres  38227  eldm4  38230  exan3  38250  exanres  38251  eldmcnv  38301  brxrn  38330  cosseq  38382  brcoss  38387  brcoss3  38389  eldm1cossres  38416  brcosscnv  38428  islshpat  38973  lshpsmreu  39065  isopos  39136  islpln5  39492  islvol5  39536  pmapjat1  39810  dibelval3  41104  diblsmopel  41128  mapdpglem3  41632  hdmapglem7a  41884  19.9dev  42207  fimgmcyc  42489  dfac11  43019  nnoeomeqom  43274  clcnvlem  43585  dfhe3  43737  ntrneineine0lem  44045  iotasbc  44388  iotasbc2  44389  fnchoice  44929  axccdom  45129  axccd  45136  stoweidlem35  45956  stoweidlem39  45960  dfatdmfcoafv2  47169  dfatco  47171  ichexmpl1  47343  ichnreuop  47346  ichreuopeq  47347  elsprel  47349  isgrim  47752  dfgric2  47768  gricushgr  47770  gricuspgr  47771  ushggricedg  47780  isubgrgrim  47781  uhgrimisgrgric  47783  grtri  47791  grtriprop  47792  isgrtri  47794  uspgrlim  47816  grlimgrtri  47820  dfgrlic2  47825  dfgrlic3  47827  grilcbri2  47828  opeliun2xp  48057  map0cor  48568  thinccic  48728  bnd2d  48773