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  3383  cgsex4gOLD  3490  ceqsex2  3495  ceqsex2v  3496  alexeqg  3607  sbc2or  3751  sbc5ALT  3771  sbcex2  3803  sbcabel  3830  elpreqprlem  4824  elpreqpr  4825  eluni  4868  csbuni  4895  intab  4935  cbvopab1  5174  cbvopab1g  5175  cbvopab1s  5177  cbvopab1v  5178  axrep1  5227  axreplem  5228  zfrepclf  5238  axsepg  5244  zfauscl  5245  sels  5395  euotd  5469  opeliunxp  5699  opeliun2xp  5700  brcog  5823  elrn2g  5847  dfdmf  5853  eldmg  5855  dmun  5867  dmopabelb  5873  dmopab2rex  5874  dm0rn0  5881  dfrnf  5907  elrnmpt1  5917  brcodir  6084  dfco2a  6212  cores  6215  sbcfung  6524  brprcneu  6832  brprcneuALT  6833  ssimaexg  6928  dmfco  6938  fndmdif  6996  fmptco  7084  fliftf  7271  imaeqsexvOLD  7319  oprabbidv  7434  cbvoprab1  7455  cbvoprab2  7456  cbvoprab12v  7458  imaeqexov  7606  uniuni  7717  dmtpos  8190  frecseq123  8234  csbfrecsg  8236  frrlem1  8238  frrlem13  8250  rdglim2  8373  ecdmn0  8698  mapsnd  8836  breng  8904  brdom2g  8906  domeng  8911  mapsnend  8985  isinf  9177  ac6sfi  9196  ordiso  9433  brwdom  9484  brwdom2  9490  zfregcl  9511  zfregclOLD  9512  inf0  9542  zfinf  9560  ttrcleq  9630  brttrcl  9634  brttrcl2  9635  ssttrcl  9636  ttrcltr  9637  ttrclss  9641  ttrclselem2  9647  bnd2  9817  isinffi  9916  acneq  9965  acni  9967  aceq0  10040  aceq3lem  10042  dfac3  10043  dfac5lem4  10048  dfac5lem4OLD  10050  dfac8  10058  dfac9  10059  kmlem1  10073  kmlem2  10074  kmlem8  10080  kmlem10  10082  kmlem13  10085  cfval  10169  cardcf  10174  cfeq0  10178  cfsuc  10179  cff1  10180  cflim3  10184  cofsmo  10191  isfin4  10219  axcc2lem  10358  axcc4dom  10363  domtriomlem  10364  dcomex  10369  axdc2lem  10370  axdc4lem  10377  zfac  10382  ac7g  10396  ac4c  10398  ac5  10399  ac6sg  10410  weth  10417  axrepndlem1  10515  axunndlem1  10518  zfcndrep  10537  zfcndinf  10541  zfcndac  10542  gruina  10741  grothomex  10752  genpass  10932  1idpr  10952  ltexprlem3  10961  ltexprlem4  10962  ltexpri  10966  reclem2pr  10971  reclem3pr  10972  recexpr  10974  infm3  12113  nnunb  12409  axdc4uz  13919  ishashinf  14398  relexpindlem  14998  sumeq1  15624  sumeq2w  15627  sumeq2ii  15628  sumeq2sdv  15638  summo  15652  fsum  15655  fsum2dlem  15705  ntrivcvgn0  15833  ntrivcvgmullem  15836  prodeq1f  15841  prodeq1  15842  prodeq2w  15845  prodeq2ii  15846  prodeq2sdv  15858  prodmo  15871  zprod  15872  fprod  15876  fprodntriv  15877  fprod2dlem  15915  vdwapun  16914  vdwmc  16918  vdwmc2  16919  isacs  17586  dfiso2  17708  brssc  17750  isssc  17756  equivestrcsetc  18087  dirge  18538  gsumvalx  18613  gsumpropd  18615  gsumpropd2lem  18616  gsumress  18619  gsumval3eu  19845  gsumval3lem2  19847  dprd2d2  19987  znleval  21521  neitr  23136  cmpcovf  23347  hausmapdom  23456  ptval  23526  elpt  23528  ptpjopn  23568  ptclsg  23571  ptcnp  23578  uffix2  23880  cnextf  24022  prdsxmslem2  24485  metustfbas  24513  metcld2  25275  dchrmusumlema  27472  dchrisum0lema  27493  elold  27867  lrrecfr  27951  istrkgld  28543  uvtx01vtx  29482  1loopgrvd2  29589  wspthsn  29933  iswspthn  29934  wspthsnon  29937  iswspthsnon  29941  wspthnon  29943  wlkiswwlks2  29960  wlkiswwlksupgr2  29962  wlklnwwlkln2lem  29967  wlksnwwlknvbij  29993  wspthsnwspthsnon  30001  elwwlks2on  30046  elwwlks2  30054  elwspths2spth  30055  clwlkclwwlk  30089  clwwlkvbij  30200  isgrpo  30585  adjeu  31977  iunrnmptss  32652  fcoinvbr  32692  2ndresdju  32739  fmptcof2  32747  acunirnmpt  32749  acunirnmpt2  32750  acunirnmpt2f  32751  aciunf1  32753  fnpreimac  32760  fpwrelmapffslem  32822  gsumwrd2dccatlem  33171  1arithidomlem1  33628  1arithidom  33630  fmcncfil  34109  bnj865  35099  bnj1388  35209  bnj1489  35232  fineqvrep  35292  fineqvac  35294  tz9.1regs  35312  satfrnmapom  35586  satf0op  35593  dmopab3rexdif  35621  prv1n  35647  rexxfr3dALT  35855  eldm3  35977  opelco3  35991  elsingles  36132  funpartlem  36158  dfrdg4  36167  linedegen  36359  prodeq12sdv  36434  cbvoprab2vw  36454  cbvoprab13vw  36457  cbvmodavw  36466  cbvopab1davw  36480  cbvopab2davw  36481  cbvoprab2davw  36488  cbvoprab12davw  36491  cbvoprab23davw  36492  cbvoprab13davw  36493  cbvsumdavw  36495  cbvproddavw  36496  cbvsumdavw2  36511  cbvproddavw2  36512  finminlem  36534  filnetlem4  36597  regsfromregtr  36690  mobidvALT  37105  bj-issetwt  37123  bj-axreprepsep  37323  bj-restuni  37350  bj-finsumval0  37540  csboprabg  37585  topdifinffinlem  37602  cbveud  37627  wl-sb8eut  37833  wl-sb8eutv  37834  sdclem1  37994  fdc  37996  ismgmOLD  38101  isriscg  38235  elrnres  38529  eldm4  38532  exan3  38551  exanres  38552  eldmcnv  38596  brxrn  38634  exeupre  38742  cosseq  38767  brcoss  38772  brcoss3  38774  eldm1cossres  38801  brcosscnv  38813  islshpat  39393  lshpsmreu  39485  isopos  39556  islpln5  39911  islvol5  39955  pmapjat1  40229  dibelval3  41523  diblsmopel  41547  mapdpglem3  42051  hdmapglem7a  42303  19.9dev  42587  fimgmcyc  42904  dfac11  43419  nnoeomeqom  43669  clcnvlem  43979  dfhe3  44131  ntrneineine0lem  44439  iotasbc  44775  iotasbc2  44776  brpermmodel  45359  permaxinf2lem  45368  permac8prim  45370  nregmodel  45373  fnchoice  45389  axccdom  45580  axccd  45587  stoweidlem35  46393  stoweidlem39  46397  dfatdmfcoafv2  47614  dfatco  47616  ichexmpl1  47829  ichnreuop  47832  ichreuopeq  47833  elsprel  47835  isgrim  48242  dfgric2  48275  gricushgr  48277  gricuspgr  48278  ushggricedg  48287  isubgrgrim  48289  uhgrimisgrgric  48291  grtri  48300  grtriprop  48301  isgrtri  48303  uspgrlim  48352  grlimedgclnbgr  48355  grlimgrtri  48363  dfgrlic2  48368  dfgrlic3  48370  grilcbri2  48371  map0cor  49214  nelsubc3lem  49429  thinccic  49830  istermc  49833  termcpropd  49862  discsntermlem  49929  basrestermcfolem  49930  discsnterm  49933  cnelsubclem  49962  bnd2d  50040