Theorem exbidv 1955

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944

This proof depends on definitions:  df-bi 210  df-ex 1812

This theorem is used by:  nfbidv  1956  2exbidv  1958  3exbidv  1959  eleq1w  2846  eleq2w  2847  eleq1d  2848  eleq2dALT  2850  clelab  2907  rexbidv2  3185  rmoeq1  3399  ceqsex2  3503  ceqsex2v  3504  alexeqg  3607  sbc2or  3750  sbc5ALT  3770  sbcex2  3801  sbcabel  3828  elpreqprlem  4823  elpreqpr  4824  eluni  4872  csbuni  4900  intab  4940  cbvopab1  5181  cbvopab1g  5182  cbvopab1s  5184  cbvopab1v  5185  axrep1  5235  axreplem  5236  zfrepclf  5246  axsepg  5252  sepg  5253  zfausclOLD  5255  sels  5411  euotd  5489  opeliunxp  5721  opeliun2xp  5722  brcog  5848  elrn2g  5876  dfdmf  5882  eldmg  5884  dmun  5896  dmopabelb  5902  dmopab2rex  5903  dm0rn0  5910  dfrnf  5936  elrnmpt1  5946  dfrn7  6071  brcodir  6118  dfco2a  6253  cores  6256  sbcfungOLD  6572  brprcneu  6883  brprcneuALT  6884  ssimaexg  6979  dmfco  6989  fndmdif  7049  fmptco  7138  fliftf  7330  oprabbidv  7493  cbvoprab1  7514  cbvoprab2  7515  cbvoprab12v  7517  imaeqexov  7666  uniuni  7783  dmtpos  8266  frecseq123  8311  csbfrecsg  8313  frrlem1  8315  frrlem13  8327  rdglim2  8451  ecdmn0  8781  mapsnd  8925  breng  8993  brdom2g  8995  domeng  9000  mapsnend  9075  isinf  9267  ac6sfi  9286  ordiso  9520  brwdom  9571  brwdom2  9577  zfregcl  9598  zfregclOLD  9599  inf0  9632  zfinf  9650  ttrcleq  9720  brttrcl  9724  brttrcl2  9725  ssttrcl  9726  ttrcltr  9727  ttrclss  9731  ttrclselem2  9737  bnd2  9966  bnd2d  9978  isinffi  10083  acneq  10132  acni  10134  aceq0  10207  aceq3lem  10209  dfac3  10210  dfac5lem4  10215  dfac8  10224  dfac9  10225  kmlem1  10239  kmlem2  10240  kmlem8  10246  kmlem10  10248  kmlem13  10251  cfval  10334  cardcf  10339  cfeq0  10344  cfsuc  10345  cff1  10346  cflim3  10350  cofsmo  10357  isfin4  10385  axcc2lem  10524  axcc4dom  10529  domtriomlem  10530  dcomex  10535  axdc2lem  10536  axdc4lem  10543  zfac  10548  ac7g  10562  ac4c  10564  ac5  10565  ac6sg  10576  weth  10583  axrepndlem1  10687  axunndlem1  10690  zfcndrep  10709  zfcndinf  10713  zfcndac  10714  gruina  10913  grothomex  10924  genpass  11104  1idpr  11124  ltexprlem3  11133  ltexprlem4  11134  ltexpri  11138  reclem2pr  11143  reclem3pr  11144  recexpr  11146  infm3  12286  nnunb  12612  axdc4uz  14137  ishashinf  14618  relexpindlem  15228  sumeq1  15868  sumeq2w  15871  sumeq2ii  15872  sumeq2sdv  15882  summo  15895  fsum  15898  fsum2dlem  15948  ntrivcvgn0  16079  ntrivcvgmullem  16082  prodeq1f  16087  prodeq1  16088  prodeq2w  16091  prodeq2ii  16092  prodeq2sdv  16103  prodmo  16115  zprod  16116  fprod  16120  fprodntriv  16121  fprod2dlem  16159  vdwapun  17164  vdwmc  17168  vdwmc2  17169  isacs  17837  dfiso2  17959  brssc  18001  isssc  18007  equivestrcsetc  18338  dirge  18789  gsumvalx  18877  gsumpropd  18879  gsumpropd2lem  18880  gsumress  18883  degenmgm2nfun  19151  gsumval3eu  20130  gsumval3lem2  20132  dprd2d2  20272  znleval  21872  neitr  23510  cmpcovf  23721  hausmapdom  23831  ptval  23901  elpt  23903  ptpjopn  23943  ptclsg  23946  ptcnp  23953  uffix2  24255  cnextf  24397  prdsxmslem2  24860  metustfbas  24888  metcld2  25640  dchrmusumlema  27832  dchrisum0lema  27853  elold  28257  lrrecfr  28341  istrkgld  28933  uvtx01vtx  29990  1loopgrvd2  30096  wspthsn  30449  iswspthn  30450  wspthsnon  30453  iswspthsnon  30457  wspthnon  30459  wlkiswwlks2  30476  wlkiswwlksupgr2  30478  wlklnwwlkln2lem  30483  wlksnwwlknvbij  30509  wspthsnwspthsnon  30517  elwwlks2on  30562  elwwlks2  30570  elwspths2spth  30571  clwlkclwwlk  30605  clwwlkvbij  30716  isgrpo  31111  adjeu  32503  iunrnmptss  33213  fcoinvbr  33253  2ndresdju  33297  fmptcof2  33305  acunirnmpt  33307  aciunf1  33311  fnpreimac  33318  fpwrelmapffslem  33377  gsumwrd2dccatlem  33691  1arithidomlem1  34120  1arithidom  34122  fmcncfil  34616  bnj865  35606  bnj1388  35716  bnj1489  35739  acwer1prclem  35830  fineqvrep  35853  fineqvac  35855  tz9.1regs  35873  onprcf1acwevdlem1  35999  satfrnmapom  36256  satf0op  36263  dmopab3rexdif  36291  prv1n  36317  rexxfr3dALT  36525  mirimanoffr  36581  eldm3  36653  opelco3  36666  elsingles  36807  funpartlem  36833  dfrdg4  36842  linedegen  37035  prodeq12sdv  37134  cbvoprab2vw  37154  cbvoprab13vw  37157  cbvmodavw  37166  cbvopab1davw  37180  cbvopab2davw  37181  cbvoprab2davw  37188  cbvoprab12davw  37191  cbvoprab23davw  37192  cbvoprab13davw  37193  cbvsumdavw  37195  cbvproddavw  37196  cbvsumdavw2  37211  cbvproddavw2  37212  finminlem  37233  filnetlem4  37296  axtco1  37388  axtco1from2  37390  axtco1g  37391  dfttc4lem1  37443  dfttc4  37445  elttcirr  37446  ttcexg  37447  regsfromregtco  37453  mh-regprimbi  37460  mh-infprim1bi  37461  mobidvALT  37896  bj-issetwt  37914  bj-inex1gALT  37964  bj-axreprepsep  38130  bj-restuni  38157  bj-finsumval0  38346  csboprabg  38393  topdifinffinlem  38410  cbveud  38435  wl-sb8eut  38650  wl-sb8eutv  38651  sdclem1  38817  fdc  38819  ismgmOLD  38924  isriscg  39058  elrnres  39350  eldm4  39353  exan3  39372  exanres  39373  eldmcnv  39417  brxrn  39455  exeupre  39563  cosseq  39588  brcoss  39593  brcoss3  39595  eldm1cossres  39622  brcosscnv  39634  islshpat  40214  lshpsmreu  40306  isopos  40377  islpln5  40732  islvol5  40776  pmapjat1  41050  dibelval3  42344  diblsmopel  42368  mapdpglem3  42872  hdmapglem7a  43124  19.9dev  43409  fimgmcyc  43738  dfac11  44204  nnoeomeqom  44454  clcnvlem  44763  dfhe3  44915  ntrneineine0lem  45223  iotasbc  45542  iotasbc2  45543  brpermmodel  46132  permaxinf2lem  46141  permac8prim  46143  nregmodel  46146  fnchoice  46185  axccdom  46374  axccd  46380  stoweidlem35  47184  stoweidlem39  47188  dfatdmfcoafv2  48463  dfatco  48465  ichexmpl1  48690  ichnreuop  48693  ichreuopeq  48694  elsprel  48696  isgrim  49119  dfgric2  49152  gricushgr  49154  gricuspgr  49155  ushggricedg  49164  isubgrgrim  49166  uhgrimisgrgric  49168  grtri  49177  grtriprop  49178  isgrtri  49180  uspgrlim  49229  grlimedgclnbgr  49232  grlimgrtri  49240  dfgrlic2  49245  dfgrlic3  49247  grilcbri2  49248  map0cor  50105  nelsubc3lem  50323  thinccic  50745  istermc  50748  termcpropd  50777  discsntermlem  50847  basrestermcfolem  50848  discsnterm  50851  cnelsubcw  50880  fuconuniqex  50925  fuconuniqex2  50926