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

Theorem exbidv 1753
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 1464 . 2  |-  ( ph  ->  A. x ph )
2 albidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2exbidh 1550 1  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103   E.wex 1426
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  ax11ev  1756  2exbidv  1796  3exbidv  1797  eubidh  1954  eubid  1955  eleq1w  2148  eleq2w  2149  eleq1  2150  eleq2  2151  rexbidv2  2383  ceqsex2  2659  alexeq  2741  ceqex  2742  sbc5  2861  sbcex2  2890  sbcexg  2891  sbcabel  2918  eluni  3651  csbunig  3656  intab  3712  cbvopab1  3903  cbvopab1s  3905  axsep2  3950  zfauscl  3951  bnd2  4000  mss  4044  opeqex  4067  euotd  4072  snnex  4262  uniuni  4264  regexmid  4341  reg2exmid  4342  onintexmid  4378  reg3exmid  4385  nnregexmid  4424  opeliunxp  4481  csbxpg  4507  brcog  4591  elrn2g  4614  dfdmf  4617  csbdmg  4618  eldmg  4619  dfrnf  4664  elrn2  4665  elrnmpt1  4674  brcodir  4806  xp11m  4856  xpimasn  4866  csbrng  4879  elxp4  4905  elxp5  4906  dfco2a  4918  cores  4921  funimaexglem  5083  brprcneu  5282  ssimaexg  5350  dmfco  5356  fndmdif  5388  fmptco  5448  fliftf  5560  acexmidlem2  5631  acexmidlemv  5632  cbvoprab1  5702  cbvoprab2  5703  dmtpos  6003  tfrlemi1  6079  tfr1onlemaccex  6095  tfrcllemaccex  6108  ecdmn0m  6314  ereldm  6315  elqsn0m  6340  mapsn  6427  bren  6444  brdomg  6445  domeng  6449  ac6sfi  6594  ordiso  6708  exmidfodomrlemr  6807  exmidfodomrlemrALT  6808  recexnq  6928  prarloc  7041  genpdflem  7045  genpassl  7062  genpassu  7063  ltexprlemell  7136  ltexprlemelu  7137  ltexprlemm  7138  recexprlemell  7160  recexprlemelu  7161  seq3f1olemp  9896  zfz1isolem1  10209  zfz1iso  10210  sumeq1  10707  sumeq2  10711  isummo  10735  fisum  10740  fsum2dlemstep  10789  bdsep2  11421  bdzfauscl  11425  strcoll2  11522  nninfall  11544
  Copyright terms: Public domain W3C validator