Theorem exbidv 1941

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

Syntax hints:   → wi 4   ↔ wb 208  ∃wex 1799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930

This theorem depends on definitions:  df-bi 209  df-ex 1800

This theorem is referenced by:  nfbidv  1942  2exbidv  1944  3exbidv  1945  eleq1w  2845  eleq2w  2846  eleq1d  2847  eleq2dALT  2849  clelab  2906  rexbidv2  3182  rmoeq1  3398  ceqsex2  3504  ceqsex2v  3505  alexeqg  3610  sbc2or  3753  sbc5ALT  3773  sbcex2  3804  sbcabel  3831  elpreqprlem  4824  elpreqpr  4825  eluni  4868  csbuni  4896  intab  4936  cbvopab1  5174  cbvopab1g  5175  cbvopab1s  5177  cbvopab1v  5178  axrep1  5228  axreplem  5229  zfrepclf  5241  axsepg  5247  zfauscl  5248  sels  5407  euotd  5482  opeliunxp  5714  opeliun2xp  5715  brcog  5838  elrn2g  5866  dfdmf  5872  eldmg  5874  dmun  5886  dmopabelb  5892  dmopab2rex  5893  dm0rn0  5900  dfrnf  5926  elrnmpt1  5936  brcodir  6106  dfco2a  6233  cores  6236  sbcfung  6545  brprcneu  6857  brprcneuALT  6858  ssimaexg  6953  dmfco  6963  fndmdif  7023  fmptco  7111  fliftf  7299  imaeqsexvOLD  7347  oprabbidv  7462  cbvoprab1  7483  cbvoprab2  7484  cbvoprab12v  7486  imaeqexov  7634  uniuni  7745  dmtpos  8218  frecseq123  8263  csbfrecsg  8265  frrlem1  8267  frrlem13  8279  rdglim2  8403  ecdmn0  8731  mapsnd  8868  breng  8936  brdom2g  8938  domeng  8943  mapsnend  9017  isinf  9209  ac6sfi  9228  ordiso  9464  brwdom  9515  brwdom2  9521  zfregcl  9542  zfregclOLD  9543  inf0  9576  zfinf  9594  ttrcleq  9664  brttrcl  9668  brttrcl2  9669  ssttrcl  9670  ttrcltr  9671  ttrclss  9675  ttrclselem2  9681  bnd2  9851  isinffi  9950  acneq  9999  acni  10001  aceq0  10074  aceq3lem  10076  dfac3  10077  dfac5lem4  10082  dfac5lem4OLD  10084  dfac8  10092  dfac9  10093  kmlem1  10107  kmlem2  10108  kmlem8  10114  kmlem10  10116  kmlem13  10119  cfval  10203  cardcf  10208  cfeq0  10213  cfsuc  10214  cff1  10215  cflim3  10219  cofsmo  10226  isfin4  10254  axcc2lem  10393  axcc4dom  10398  domtriomlem  10399  dcomex  10404  axdc2lem  10405  axdc4lem  10412  zfac  10417  ac7g  10431  ac4c  10433  ac5  10434  ac6sg  10445  weth  10452  axrepndlem1  10550  axunndlem1  10553  zfcndrep  10572  zfcndinf  10576  zfcndac  10577  gruina  10776  grothomex  10787  genpass  10967  1idpr  10987  ltexprlem3  10996  ltexprlem4  10997  ltexpri  11001  reclem2pr  11006  reclem3pr  11007  recexpr  11009  infm3  12151  nnunb  12477  axdc4uz  13997  ishashinf  14476  relexpindlem  15076  sumeq1  15716  sumeq2w  15719  sumeq2ii  15720  sumeq2sdv  15730  summo  15744  fsum  15747  fsum2dlem  15797  ntrivcvgn0  15928  ntrivcvgmullem  15931  prodeq1f  15936  prodeq1  15937  prodeq2w  15940  prodeq2ii  15941  prodeq2sdv  15953  prodmo  15966  zprod  15967  fprod  15971  fprodntriv  15972  fprod2dlem  16010  vdwapun  17010  vdwmc  17014  vdwmc2  17015  isacs  17683  dfiso2  17805  brssc  17847  isssc  17853  equivestrcsetc  18184  dirge  18635  gsumvalx  18710  gsumpropd  18712  gsumpropd2lem  18713  gsumress  18716  gsumval3eu  19944  gsumval3lem2  19946  dprd2d2  20086  znleval  21606  neitr  23240  cmpcovf  23451  hausmapdom  23560  ptval  23630  elpt  23632  ptpjopn  23672  ptclsg  23675  ptcnp  23682  uffix2  23984  cnextf  24126  prdsxmslem2  24589  metustfbas  24617  metcld2  25369  dchrmusumlema  27557  dchrisum0lema  27578  elold  27952  lrrecfr  28036  istrkgld  28628  uvtx01vtx  29598  1loopgrvd2  29704  wspthsn  30048  iswspthn  30049  wspthsnon  30052  iswspthsnon  30056  wspthnon  30058  wlkiswwlks2  30075  wlkiswwlksupgr2  30077  wlklnwwlkln2lem  30082  wlksnwwlknvbij  30108  wspthsnwspthsnon  30116  elwwlks2on  30161  elwwlks2  30169  elwspths2spth  30170  clwlkclwwlk  30204  clwwlkvbij  30315  isgrpo  30700  adjeu  32092  iunrnmptss  32765  fcoinvbr  32805  2ndresdju  32851  fmptcof2  32859  acunirnmpt  32861  acunirnmpt2  32862  acunirnmpt2f  32863  aciunf1  32865  fnpreimac  32872  fpwrelmapffslem  32934  gsumwrd2dccatlem  33257  1arithidomlem1  33731  1arithidom  33733  fmcncfil  34228  bnj865  35218  bnj1388  35328  bnj1489  35351  fineqvrep  35410  fineqvac  35412  tz9.1regs  35430  satfrnmapom  35720  satf0op  35727  dmopab3rexdif  35755  prv1n  35781  rexxfr3dALT  35989  eldm3  36111  opelco3  36125  elsingles  36266  funpartlem  36292  dfrdg4  36301  linedegen  36493  prodeq12sdv  36578  cbvoprab2vw  36598  cbvoprab13vw  36601  cbvmodavw  36610  cbvopab1davw  36624  cbvopab2davw  36625  cbvoprab2davw  36632  cbvoprab12davw  36635  cbvoprab23davw  36636  cbvoprab13davw  36637  cbvsumdavw  36639  cbvproddavw  36640  cbvsumdavw2  36655  cbvproddavw2  36656  finminlem  36678  filnetlem4  36741  axtco1  36833  axtco1from2  36835  axtco1g  36836  dfttc4lem1  36888  dfttc4  36890  elttcirr  36891  ttcexg  36892  regsfromregtco  36898  mh-regprimbi  36905  mh-infprim1bi  36906  mobidvALT  37342  bj-issetwt  37360  bj-axreprepsep  37560  bj-restuni  37587  bj-finsumval0  37777  csboprabg  37824  topdifinffinlem  37841  cbveud  37866  wl-sb8eut  38081  wl-sb8eutv  38082  sdclem1  38242  fdc  38244  ismgmOLD  38349  isriscg  38483  elrnres  38777  eldm4  38780  exan3  38799  exanres  38800  eldmcnv  38844  brxrn  38882  exeupre  38990  cosseq  39015  brcoss  39020  brcoss3  39022  eldm1cossres  39049  brcosscnv  39061  islshpat  39641  lshpsmreu  39733  isopos  39804  islpln5  40159  islvol5  40203  pmapjat1  40477  dibelval3  41771  diblsmopel  41795  mapdpglem3  42299  hdmapglem7a  42551  19.9dev  42834  fimgmcyc  43152  dfac11  43639  nnoeomeqom  43889  clcnvlem  44199  dfhe3  44351  ntrneineine0lem  44659  iotasbc  44995  iotasbc2  44996  brpermmodel  45579  permaxinf2lem  45588  permac8prim  45590  nregmodel  45593  fnchoice  45609  axccdom  45798  axccd  45804  stoweidlem35  46609  stoweidlem39  46613  dfatdmfcoafv2  47848  dfatco  47850  ichexmpl1  48075  ichnreuop  48078  ichreuopeq  48079  elsprel  48081  isgrim  48504  dfgric2  48537  gricushgr  48539  gricuspgr  48540  ushggricedg  48549  isubgrgrim  48551  uhgrimisgrgric  48553  grtri  48562  grtriprop  48563  isgrtri  48565  uspgrlim  48614  grlimedgclnbgr  48617  grlimgrtri  48625  dfgrlic2  48630  dfgrlic3  48632  grilcbri2  48633  map0cor  49476  nelsubc3lem  49691  thinccic  50092  istermc  50095  termcpropd  50124  discsntermlem  50191  basrestermcfolem  50192  discsnterm  50195  cnelsubclem  50224  bnd2d  50302