Theorem exbidv 1923

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  nfbidv  1924  2exbidv  1926  3exbidv  1927  eleq1w  2820  eleq2w  2821  eleq1d  2822  eleq2dALT  2824  clelab  2881  rexbidv2  3158  rmoeq1  3374  ceqsex2  3482  ceqsex2v  3483  alexeqg  3594  sbc2or  3738  sbc5ALT  3758  sbcex2  3790  sbcabel  3817  elpreqprlem  4810  elpreqpr  4811  eluni  4854  csbuni  4881  intab  4921  cbvopab1  5160  cbvopab1g  5161  cbvopab1s  5163  cbvopab1v  5164  axrep1  5214  axreplem  5215  zfrepclf  5227  axsepg  5233  zfauscl  5234  sels  5388  euotd  5462  opeliunxp  5692  opeliun2xp  5693  brcog  5816  elrn2g  5840  dfdmf  5846  eldmg  5848  dmun  5860  dmopabelb  5866  dmopab2rex  5867  dm0rn0  5874  dfrnf  5900  elrnmpt1  5910  brcodir  6077  dfco2a  6205  cores  6208  sbcfung  6517  brprcneu  6825  brprcneuALT  6826  ssimaexg  6921  dmfco  6931  fndmdif  6989  fmptco  7077  fliftf  7264  imaeqsexvOLD  7312  oprabbidv  7427  cbvoprab1  7448  cbvoprab2  7449  cbvoprab12v  7451  imaeqexov  7599  uniuni  7710  dmtpos  8182  frecseq123  8226  csbfrecsg  8228  frrlem1  8230  frrlem13  8242  rdglim2  8365  ecdmn0  8690  mapsnd  8828  breng  8896  brdom2g  8898  domeng  8903  mapsnend  8977  isinf  9169  ac6sfi  9188  ordiso  9425  brwdom  9476  brwdom2  9482  zfregcl  9503  zfregclOLD  9504  inf0  9536  zfinf  9554  ttrcleq  9624  brttrcl  9628  brttrcl2  9629  ssttrcl  9630  ttrcltr  9631  ttrclss  9635  ttrclselem2  9641  bnd2  9811  isinffi  9910  acneq  9959  acni  9961  aceq0  10034  aceq3lem  10036  dfac3  10037  dfac5lem4  10042  dfac5lem4OLD  10044  dfac8  10052  dfac9  10053  kmlem1  10067  kmlem2  10068  kmlem8  10074  kmlem10  10076  kmlem13  10079  cfval  10163  cardcf  10168  cfeq0  10172  cfsuc  10173  cff1  10174  cflim3  10178  cofsmo  10185  isfin4  10213  axcc2lem  10352  axcc4dom  10357  domtriomlem  10358  dcomex  10363  axdc2lem  10364  axdc4lem  10371  zfac  10376  ac7g  10390  ac4c  10392  ac5  10393  ac6sg  10404  weth  10411  axrepndlem1  10509  axunndlem1  10512  zfcndrep  10531  zfcndinf  10535  zfcndac  10536  gruina  10735  grothomex  10746  genpass  10926  1idpr  10946  ltexprlem3  10955  ltexprlem4  10956  ltexpri  10960  reclem2pr  10965  reclem3pr  10966  recexpr  10968  infm3  12109  nnunb  12427  axdc4uz  13940  ishashinf  14419  relexpindlem  15019  sumeq1  15645  sumeq2w  15648  sumeq2ii  15649  sumeq2sdv  15659  summo  15673  fsum  15676  fsum2dlem  15726  ntrivcvgn0  15857  ntrivcvgmullem  15860  prodeq1f  15865  prodeq1  15866  prodeq2w  15869  prodeq2ii  15870  prodeq2sdv  15882  prodmo  15895  zprod  15896  fprod  15900  fprodntriv  15901  fprod2dlem  15939  vdwapun  16939  vdwmc  16943  vdwmc2  16944  isacs  17611  dfiso2  17733  brssc  17775  isssc  17781  equivestrcsetc  18112  dirge  18563  gsumvalx  18638  gsumpropd  18640  gsumpropd2lem  18641  gsumress  18644  gsumval3eu  19873  gsumval3lem2  19875  dprd2d2  20015  znleval  21547  neitr  23158  cmpcovf  23369  hausmapdom  23478  ptval  23548  elpt  23550  ptpjopn  23590  ptclsg  23593  ptcnp  23600  uffix2  23902  cnextf  24044  prdsxmslem2  24507  metustfbas  24535  metcld2  25287  dchrmusumlema  27473  dchrisum0lema  27494  elold  27868  lrrecfr  27952  istrkgld  28544  uvtx01vtx  29483  1loopgrvd2  29590  wspthsn  29934  iswspthn  29935  wspthsnon  29938  iswspthsnon  29942  wspthnon  29944  wlkiswwlks2  29961  wlkiswwlksupgr2  29963  wlklnwwlkln2lem  29968  wlksnwwlknvbij  29994  wspthsnwspthsnon  30002  elwwlks2on  30047  elwwlks2  30055  elwspths2spth  30056  clwlkclwwlk  30090  clwwlkvbij  30201  isgrpo  30586  adjeu  31978  iunrnmptss  32653  fcoinvbr  32693  2ndresdju  32740  fmptcof2  32748  acunirnmpt  32750  acunirnmpt2  32751  acunirnmpt2f  32752  aciunf1  32754  fnpreimac  32761  fpwrelmapffslem  32823  gsumwrd2dccatlem  33156  1arithidomlem1  33613  1arithidom  33615  fmcncfil  34094  bnj865  35084  bnj1388  35194  bnj1489  35217  fineqvrep  35277  fineqvac  35279  tz9.1regs  35297  satfrnmapom  35571  satf0op  35578  dmopab3rexdif  35606  prv1n  35632  rexxfr3dALT  35840  eldm3  35962  opelco3  35976  elsingles  36117  funpartlem  36143  dfrdg4  36152  linedegen  36344  prodeq12sdv  36419  cbvoprab2vw  36439  cbvoprab13vw  36442  cbvmodavw  36451  cbvopab1davw  36465  cbvopab2davw  36466  cbvoprab2davw  36473  cbvoprab12davw  36476  cbvoprab23davw  36477  cbvoprab13davw  36478  cbvsumdavw  36480  cbvproddavw  36481  cbvsumdavw2  36496  cbvproddavw2  36497  finminlem  36519  filnetlem4  36582  axtco1  36674  axtco1from2  36676  axtco1g  36677  dfttc4lem1  36729  dfttc4  36731  elttcirr  36732  ttcexg  36733  regsfromregtco  36739  mh-regprimbi  36746  mh-infprim1bi  36747  mobidvALT  37183  bj-issetwt  37201  bj-axreprepsep  37401  bj-restuni  37428  bj-finsumval0  37618  csboprabg  37663  topdifinffinlem  37680  cbveud  37705  wl-sb8eut  37920  wl-sb8eutv  37921  sdclem1  38081  fdc  38083  ismgmOLD  38188  isriscg  38322  elrnres  38616  eldm4  38619  exan3  38638  exanres  38639  eldmcnv  38683  brxrn  38721  exeupre  38829  cosseq  38854  brcoss  38859  brcoss3  38861  eldm1cossres  38888  brcosscnv  38900  islshpat  39480  lshpsmreu  39572  isopos  39643  islpln5  39998  islvol5  40042  pmapjat1  40316  dibelval3  41610  diblsmopel  41634  mapdpglem3  42138  hdmapglem7a  42390  19.9dev  42673  fimgmcyc  42996  dfac11  43511  nnoeomeqom  43761  clcnvlem  44071  dfhe3  44223  ntrneineine0lem  44531  iotasbc  44867  iotasbc2  44868  brpermmodel  45451  permaxinf2lem  45460  permac8prim  45462  nregmodel  45465  fnchoice  45481  axccdom  45672  axccd  45679  stoweidlem35  46484  stoweidlem39  46488  dfatdmfcoafv2  47717  dfatco  47719  ichexmpl1  47944  ichnreuop  47947  ichreuopeq  47948  elsprel  47950  isgrim  48373  dfgric2  48406  gricushgr  48408  gricuspgr  48409  ushggricedg  48418  isubgrgrim  48420  uhgrimisgrgric  48422  grtri  48431  grtriprop  48432  isgrtri  48434  uspgrlim  48483  grlimedgclnbgr  48486  grlimgrtri  48494  dfgrlic2  48499  dfgrlic3  48501  grilcbri2  48502  map0cor  49345  nelsubc3lem  49560  thinccic  49961  istermc  49964  termcpropd  49993  discsntermlem  50060  basrestermcfolem  50061  discsnterm  50064  cnelsubclem  50093  bnd2d  50171