Theorem exbidv 1880

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

Syntax hints:   → wi 4   ↔ wb 198  ∃wex 1742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869

This theorem depends on definitions:  df-bi 199  df-ex 1743

This theorem is referenced by:  nfbidv  1881  2exbidv  1883  3exbidv  1884  mobiOLD  2557  mobidOLD  2563  eubidvOLD  2620  mobidvOLDOLD  2621  eubidOLDOLD  2626  eleq1w  2842  eleq2w  2843  eleq1d  2844  eleq2dALT  2846  rexbidv2  3234  ceqsex2  3458  ceqsex2v  3459  alexeqg  3553  sbc2or  3684  sbc5  3700  sbcex2  3731  sbcabel  3758  elpreqprlem  4666  elpreqpr  4667  eluni  4711  csbuni  4736  intab  4775  cbvopab1  4998  cbvopab1s  5000  axrep1  5046  axreplem  5047  zfrepclf  5052  axsep2  5057  zfauscl  5058  euotd  5255  opeliunxp  5465  brcog  5583  elrn2g  5607  dfdmf  5611  eldmg  5613  dfrnf  5660  elrn2  5661  elrnmpt1  5670  brcodir  5816  dfco2a  5935  cores  5938  sbcfung  6209  brprcneu  6488  ssimaexg  6575  dmfco  6583  fndmdif  6635  fmptco  6712  fliftf  6889  cbvoprab1  7055  cbvoprab2  7056  uniuni  7299  dmtpos  7705  wrecseq123  7749  wfrlem1  7755  wfrlem3a  7758  wfrlem15  7771  rdglim2  7870  ecdmn0  8134  mapsnd  8246  bren  8313  brdomg  8314  domeng  8318  mapsnend  8383  isinf  8524  ac6sfi  8555  ordiso  8773  brwdom  8824  brwdom2  8830  zfregcl  8851  inf0  8876  zfinf  8894  bnd2  9114  isinffi  9213  acneq  9261  acni  9263  aceq0  9336  aceq3lem  9338  dfac3  9339  dfac5lem4  9344  dfac8  9353  dfac9  9354  kmlem1  9368  kmlem2  9369  kmlem8  9375  kmlem10  9377  kmlem13  9380  cfval  9465  cardcf  9470  cfeq0  9474  cfsuc  9475  cff1  9476  cflim3  9480  cofsmo  9487  isfin4  9515  axcc2lem  9654  axcc4dom  9659  domtriomlem  9660  dcomex  9665  axdc2lem  9666  axdc4lem  9673  zfac  9678  ac7g  9692  ac4c  9694  ac5  9695  ac6sg  9706  weth  9713  axrepndlem1  9810  axunndlem1  9813  zfcndrep  9832  zfcndinf  9836  zfcndac  9837  gruina  10036  grothomex  10047  genpass  10227  1idpr  10247  ltexprlem3  10256  ltexprlem4  10257  ltexpri  10261  reclem2pr  10266  reclem3pr  10267  recexpr  10269  infm3  11399  nnunb  11701  axdc4uz  13165  ishashinf  13632  relexpindlem  14281  sumeq1  14904  sumeq2w  14907  sumeq2ii  14908  summo  14932  fsum  14935  fsum2dlem  14983  ntrivcvgn0  15112  ntrivcvgmullem  15115  prodeq1f  15120  prodeq2w  15124  prodeq2ii  15125  prodmo  15148  zprod  15149  fprod  15153  fprodntriv  15154  fprod2dlem  15192  vdwapun  16164  vdwmc  16168  vdwmc2  16169  isacs  16792  dfiso2  16912  brssc  16954  isssc  16960  equivestrcsetc  17272  dirge  17717  gsumvalx  17750  gsumpropd  17752  gsumpropd2lem  17753  gsumress  17756  gsumval3eu  18790  gsumval3lem2  18792  dprd2d2  18928  znleval  20415  neitr  21504  cmpcovf  21715  hausmapdom  21824  ptval  21894  elpt  21896  ptpjopn  21936  ptclsg  21939  ptcnp  21946  uffix2  22248  cnextf  22390  prdsxmslem2  22854  metustfbas  22882  metcld2  23625  dchrmusumlema  25783  dchrisum0lema  25804  istrkgld  25959  uvtx01vtx  26894  1loopgrvd2  27000  wspthsn  27346  iswspthn  27347  wspthsnon  27350  iswspthsnon  27354  wspthnon  27356  wlkiswwlks2  27373  wlkiswwlksupgr2  27375  wlklnwwlkln2lem  27381  wlksnwwlknvbij  27420  wspthsnwspthsnon  27434  elwwlks2on  27477  elwwlks2  27484  elwspths2spth  27485  clwlkclwwlk  27520  clwlkclwwlkOLD  27521  clwwlkvbij  27653  clwwlkvbijOLD  27654  isgrpo  28063  adjeu  29459  iunrnmptss  30100  fcoinvbr  30136  fmptcof2  30178  acunirnmpt  30180  acunirnmpt2  30181  acunirnmpt2f  30182  aciunf1  30184  fnpreimac  30192  fpwrelmapffslem  30241  fmcncfil  30847  bnj865  31871  bnj1388  31979  bnj1489  32002  satf0op  32216  eldm3  32546  opelco3  32567  frecseq123  32669  frrlem1  32673  frrlem13  32685  elsingles  32929  funpartlem  32953  dfrdg4  32962  linedegen  33154  finminlem  33216  filnetlem4  33279  bj-axrep1  33647  bj-axrep2  33648  bj-axrep3  33649  mobidvALT  33701  bj-issetwt  33711  bj-axsep2  33766  bj-restuni  33927  bj-finsumval0  34059  csbwrecsg  34079  csboprabg  34082  topdifinffinlem  34099  cbveud  34124  wl-sb8eut  34283  wl-dfrmof  34325  sdclem1  34489  fdc  34491  ismgmOLD  34599  isriscg  34733  eldm4  35004  exan3  35024  exanres  35025  eldmcnv  35077  brxrn  35100  cosseq  35145  brcoss  35150  brcoss3  35152  eldm1cossres  35174  brcosscnv  35186  islshpat  35627  lshpsmreu  35719  isopos  35790  islpln5  36145  islvol5  36189  pmapjat1  36463  dibelval3  37757  diblsmopel  37781  mapdpglem3  38285  hdmapglem7a  38537  dfac11  39087  clcnvlem  39375  dfhe3  39513  ntrneineine0lem  39825  iotasbc  40197  iotasbc2  40198  fnchoice  40734  axccdom  40938  axccd  40947  stoweidlem35  41776  stoweidlem39  41780  dfatdmfcoafv2  42884  dfatco  42886  ichexmpl1  43024  ichnreuop  43027  ichreuopeq  43028  elsprel  43030  isomgr  43381  isomgreqve  43383  isomushgr  43384  isomuspgr  43392  isomgrsym  43394  isomgrtr  43397  ushrisomgr  43399  opeliun2xp  43770  bnd2d  44176