Theorem exbidv 1921

Description: Formula-building rule for existential quantifier (deduction form). See also exbidh 1867 and exbid 2223. (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  2817  eleq2w  2818  eleq1d  2819  eleq2dALT  2821  clelab  2880  rexbidv2  3160  rmoeq1  3395  cgsex4gOLD  3508  ceqsex2  3514  ceqsex2v  3515  alexeqg  3630  sbc2or  3774  sbc5ALT  3794  sbcex2  3826  sbcabel  3853  elpreqprlem  4842  elpreqpr  4843  eluni  4886  csbuni  4912  intab  4954  cbvopab1  5193  cbvopab1g  5194  cbvopab1s  5196  cbvopab1v  5197  axrep1  5250  axreplem  5251  zfrepclf  5261  axsepg  5267  zfauscl  5268  sels  5413  euotd  5488  opeliunxp  5721  opeliun2xp  5722  brcog  5846  elrn2g  5870  dfdmf  5876  eldmg  5878  dmopabelb  5896  dmopab2rex  5897  dfrnf  5930  elrnmpt1  5940  brcodir  6108  dfco2a  6235  cores  6238  sbcfung  6560  brprcneu  6866  brprcneuALT  6867  ssimaexg  6965  dmfco  6975  fndmdif  7032  fmptco  7119  fliftf  7308  imaeqsexvOLD  7356  oprabbidv  7473  cbvoprab1  7494  cbvoprab2  7495  cbvoprab12v  7497  imaeqexov  7645  uniuni  7756  dmtpos  8237  frecseq123  8281  csbfrecsg  8283  frrlem1  8285  frrlem13  8297  wrecseq123OLD  8314  wfrlem1OLD  8322  wfrlem3OLDa  8325  wfrlem15OLD  8337  rdglim2  8446  ecdmn0  8768  mapsnd  8900  breng  8968  brdom2g  8970  brdomgOLD  8972  domeng  8977  mapsnend  9050  isinf  9268  isinfOLD  9269  ac6sfi  9292  ordiso  9530  brwdom  9581  brwdom2  9587  zfregcl  9608  inf0  9635  zfinf  9653  ttrcleq  9723  brttrcl  9727  brttrcl2  9728  ssttrcl  9729  ttrcltr  9730  ttrclss  9734  ttrclselem2  9740  bnd2  9907  isinffi  10006  acneq  10057  acni  10059  aceq0  10132  aceq3lem  10134  dfac3  10135  dfac5lem4  10140  dfac5lem4OLD  10142  dfac8  10150  dfac9  10151  kmlem1  10165  kmlem2  10166  kmlem8  10172  kmlem10  10174  kmlem13  10177  cfval  10261  cardcf  10266  cfeq0  10270  cfsuc  10271  cff1  10272  cflim3  10276  cofsmo  10283  isfin4  10311  axcc2lem  10450  axcc4dom  10455  domtriomlem  10456  dcomex  10461  axdc2lem  10462  axdc4lem  10469  zfac  10474  ac7g  10488  ac4c  10490  ac5  10491  ac6sg  10502  weth  10509  axrepndlem1  10606  axunndlem1  10609  zfcndrep  10628  zfcndinf  10632  zfcndac  10633  gruina  10832  grothomex  10843  genpass  11023  1idpr  11043  ltexprlem3  11052  ltexprlem4  11053  ltexpri  11057  reclem2pr  11062  reclem3pr  11063  recexpr  11065  infm3  12201  nnunb  12497  axdc4uz  14002  ishashinf  14481  relexpindlem  15082  sumeq1  15705  sumeq2w  15708  sumeq2ii  15709  sumeq2sdv  15719  summo  15733  fsum  15736  fsum2dlem  15786  ntrivcvgn0  15914  ntrivcvgmullem  15917  prodeq1f  15922  prodeq1  15923  prodeq2w  15926  prodeq2ii  15927  prodeq2sdv  15939  prodmo  15952  zprod  15953  fprod  15957  fprodntriv  15958  fprod2dlem  15996  vdwapun  16994  vdwmc  16998  vdwmc2  16999  isacs  17663  dfiso2  17785  brssc  17827  isssc  17833  equivestrcsetc  18164  dirge  18613  gsumvalx  18654  gsumpropd  18656  gsumpropd2lem  18657  gsumress  18660  gsumval3eu  19885  gsumval3lem2  19887  dprd2d2  20027  znleval  21515  neitr  23118  cmpcovf  23329  hausmapdom  23438  ptval  23508  elpt  23510  ptpjopn  23550  ptclsg  23553  ptcnp  23560  uffix2  23862  cnextf  24004  prdsxmslem2  24468  metustfbas  24496  metcld2  25259  dchrmusumlema  27456  dchrisum0lema  27477  elold  27833  lrrecfr  27902  istrkgld  28438  uvtx01vtx  29376  1loopgrvd2  29483  wspthsn  29830  iswspthn  29831  wspthsnon  29834  iswspthsnon  29838  wspthnon  29840  wlkiswwlks2  29857  wlkiswwlksupgr2  29859  wlklnwwlkln2lem  29864  wlksnwwlknvbij  29890  wspthsnwspthsnon  29898  elwwlks2on  29941  elwwlks2  29948  elwspths2spth  29949  clwlkclwwlk  29983  clwwlkvbij  30094  isgrpo  30478  adjeu  31870  iunrnmptss  32546  fcoinvbr  32586  2ndresdju  32627  fmptcof2  32635  acunirnmpt  32637  acunirnmpt2  32638  acunirnmpt2f  32639  aciunf1  32641  fnpreimac  32649  fpwrelmapffslem  32709  gsumwrd2dccatlem  33060  1arithidomlem1  33550  1arithidom  33552  fmcncfil  33962  bnj865  34954  bnj1388  35064  bnj1489  35087  fineqvrep  35126  fineqvac  35128  satfrnmapom  35392  satf0op  35399  dmopab3rexdif  35427  prv1n  35453  rexxfr3dALT  35661  eldm3  35778  opelco3  35792  elsingles  35936  funpartlem  35960  dfrdg4  35969  linedegen  36161  prodeq12sdv  36236  cbvoprab2vw  36256  cbvoprab13vw  36259  cbvmodavw  36268  cbvopab1davw  36282  cbvopab2davw  36283  cbvoprab2davw  36290  cbvoprab12davw  36293  cbvoprab23davw  36294  cbvoprab13davw  36295  cbvsumdavw  36297  cbvproddavw  36298  cbvsumdavw2  36313  cbvproddavw2  36314  finminlem  36336  filnetlem4  36399  mobidvALT  36875  bj-issetwt  36893  bj-restuni  37115  bj-finsumval0  37303  csboprabg  37348  topdifinffinlem  37365  cbveud  37390  wl-sb8eut  37596  wl-sb8eutv  37597  sdclem1  37767  fdc  37769  ismgmOLD  37874  isriscg  38008  elrnres  38289  eldm4  38292  exan3  38312  exanres  38313  eldmcnv  38363  brxrn  38392  cosseq  38444  brcoss  38449  brcoss3  38451  eldm1cossres  38478  brcosscnv  38490  islshpat  39035  lshpsmreu  39127  isopos  39198  islpln5  39554  islvol5  39598  pmapjat1  39872  dibelval3  41166  diblsmopel  41190  mapdpglem3  41694  hdmapglem7a  41946  19.9dev  42265  fimgmcyc  42557  dfac11  43086  nnoeomeqom  43336  clcnvlem  43647  dfhe3  43799  ntrneineine0lem  44107  iotasbc  44443  iotasbc2  44444  brpermmodel  45028  permaxinf2lem  45037  fnchoice  45053  axccdom  45246  axccd  45253  stoweidlem35  46064  stoweidlem39  46068  dfatdmfcoafv2  47283  dfatco  47285  ichexmpl1  47483  ichnreuop  47486  ichreuopeq  47487  elsprel  47489  isgrim  47895  dfgric2  47928  gricushgr  47930  gricuspgr  47931  ushggricedg  47940  isubgrgrim  47942  uhgrimisgrgric  47944  grtri  47952  grtriprop  47953  isgrtri  47955  uspgrlim  48004  grlimgrtri  48008  dfgrlic2  48013  dfgrlic3  48015  grilcbri2  48016  map0cor  48833  nelsubc3lem  49037  thinccic  49357  istermc  49360  termcpropd  49388  discsntermlem  49447  basrestermcfolem  49448  discsnterm  49451  cnelsubclem  49480  bnd2d  49545