ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  exbidv Unicode version

Theorem exbidv 1825
Description: Formula-building rule for existential quantifier (deduction form). (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
albidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
exbidv  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)

Proof of Theorem exbidv
StepHypRef Expression
1 ax-17 1526 . 2  |-  ( ph  ->  A. x ph )
2 albidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2exbidh 1614 1  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105   E.wex 1492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  ax11ev  1828  2exbidv  1868  3exbidv  1869  eubidh  2032  eubid  2033  eleq1w  2238  eleq2w  2239  eleq1  2240  eleq2  2241  rexbidv2  2480  ceqsex2  2777  alexeq  2863  ceqex  2864  sbc5  2986  sbcex2  3016  sbcexg  3017  sbcabel  3044  eluni  3810  csbunig  3815  intab  3871  cbvopab1  4073  cbvopab1s  4075  axsep2  4119  zfauscl  4120  bnd2  4170  mss  4223  opeqex  4246  euotd  4251  snnex  4445  uniuni  4448  regexmid  4531  reg2exmid  4532  onintexmid  4569  reg3exmid  4576  nnregexmid  4617  opeliunxp  4678  csbxpg  4704  brcog  4790  elrn2g  4813  dfdmf  4816  csbdmg  4817  eldmg  4818  dfrnf  4864  elrn2  4865  elrnmpt1  4874  brcodir  5012  xp11m  5063  xpimasn  5073  csbrng  5086  elxp4  5112  elxp5  5113  dfco2a  5125  cores  5128  funimaexglem  5295  brprcneu  5504  ssimaexg  5574  dmfco  5580  fndmdif  5617  fmptco  5678  fliftf  5794  acexmidlem2  5866  acexmidlemv  5867  cbvoprab1  5941  cbvoprab2  5942  oprssdmm  6166  dmtpos  6251  tfrlemi1  6327  tfr1onlemaccex  6343  tfrcllemaccex  6356  ecdmn0m  6571  ereldm  6572  elqsn0m  6597  mapsn  6684  bren  6741  brdomg  6742  domeng  6746  ac6sfi  6892  ordiso  7029  ctssdclemr  7105  enumct  7108  ctssexmid  7142  exmidfodomrlemr  7195  exmidfodomrlemrALT  7196  acfun  7200  ccfunen  7251  cc1  7252  cc2lem  7253  cc2  7254  cc3  7255  recexnq  7377  prarloc  7490  genpdflem  7494  genpassl  7511  genpassu  7512  ltexprlemell  7585  ltexprlemelu  7586  ltexprlemm  7587  recexprlemell  7609  recexprlemelu  7610  cnm  7819  sup3exmid  8900  seq3f1olemp  10485  zfz1isolem1  10801  zfz1iso  10802  sumeq1  11344  sumeq2  11348  summodc  11372  fsum3  11376  fsum2dlemstep  11423  ntrivcvgap0  11538  prodeq1f  11541  prodeq2w  11545  prodeq2  11546  prodmodc  11567  zproddc  11568  fprodseq  11572  fprodntrivap  11573  fprod2dlemstep  11611  ctinf  12411  ctiunct  12421  ssomct  12426  bdsep2  14287  bdzfauscl  14291  strcoll2  14384  sscoll2  14389  subctctexmid  14399  nninfall  14407
  Copyright terms: Public domain W3C validator