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

Theorem exbidv 1781
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 1491 . 2  |-  ( ph  ->  A. x ph )
2 albidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2exbidh 1578 1  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104   E.wex 1453
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  ax11ev  1784  2exbidv  1824  3exbidv  1825  eubidh  1983  eubid  1984  eleq1w  2178  eleq2w  2179  eleq1  2180  eleq2  2181  rexbidv2  2417  ceqsex2  2700  alexeq  2785  ceqex  2786  sbc5  2905  sbcex2  2934  sbcexg  2935  sbcabel  2962  eluni  3709  csbunig  3714  intab  3770  cbvopab1  3971  cbvopab1s  3973  axsep2  4017  zfauscl  4018  bnd2  4067  mss  4118  opeqex  4141  euotd  4146  snnex  4339  uniuni  4342  regexmid  4420  reg2exmid  4421  onintexmid  4457  reg3exmid  4464  nnregexmid  4504  opeliunxp  4564  csbxpg  4590  brcog  4676  elrn2g  4699  dfdmf  4702  csbdmg  4703  eldmg  4704  dfrnf  4750  elrn2  4751  elrnmpt1  4760  brcodir  4896  xp11m  4947  xpimasn  4957  csbrng  4970  elxp4  4996  elxp5  4997  dfco2a  5009  cores  5012  funimaexglem  5176  brprcneu  5382  ssimaexg  5451  dmfco  5457  fndmdif  5493  fmptco  5554  fliftf  5668  acexmidlem2  5739  acexmidlemv  5740  cbvoprab1  5811  cbvoprab2  5812  oprssdmm  6037  dmtpos  6121  tfrlemi1  6197  tfr1onlemaccex  6213  tfrcllemaccex  6226  ecdmn0m  6439  ereldm  6440  elqsn0m  6465  mapsn  6552  bren  6609  brdomg  6610  domeng  6614  ac6sfi  6760  ordiso  6889  ctssdclemr  6965  enumct  6968  ctssexmid  6992  exmidfodomrlemr  7026  exmidfodomrlemrALT  7027  acfun  7031  ccfunen  7047  recexnq  7166  prarloc  7279  genpdflem  7283  genpassl  7300  genpassu  7301  ltexprlemell  7374  ltexprlemelu  7375  ltexprlemm  7376  recexprlemell  7398  recexprlemelu  7399  cnm  7608  sup3exmid  8683  seq3f1olemp  10243  zfz1isolem1  10551  zfz1iso  10552  sumeq1  11092  sumeq2  11096  summodc  11120  fsum3  11124  fsum2dlemstep  11171  ctinf  11870  ctiunct  11880  bdsep2  13011  bdzfauscl  13015  strcoll2  13108  subctctexmid  13123  nninfall  13131
  Copyright terms: Public domain W3C validator