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

Theorem exbidv 1779
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 1489 . 2  |-  ( ph  ->  A. x ph )
2 albidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2exbidh 1576 1  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104   E.wex 1451
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 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  ax11ev  1782  2exbidv  1822  3exbidv  1823  eubidh  1981  eubid  1982  eleq1w  2176  eleq2w  2177  eleq1  2178  eleq2  2179  rexbidv2  2415  ceqsex2  2698  alexeq  2783  ceqex  2784  sbc5  2903  sbcex2  2932  sbcexg  2933  sbcabel  2960  eluni  3707  csbunig  3712  intab  3768  cbvopab1  3969  cbvopab1s  3971  axsep2  4015  zfauscl  4016  bnd2  4065  mss  4116  opeqex  4139  euotd  4144  snnex  4337  uniuni  4340  regexmid  4418  reg2exmid  4419  onintexmid  4455  reg3exmid  4462  nnregexmid  4502  opeliunxp  4562  csbxpg  4588  brcog  4674  elrn2g  4697  dfdmf  4700  csbdmg  4701  eldmg  4702  dfrnf  4748  elrn2  4749  elrnmpt1  4758  brcodir  4894  xp11m  4945  xpimasn  4955  csbrng  4968  elxp4  4994  elxp5  4995  dfco2a  5007  cores  5010  funimaexglem  5174  brprcneu  5380  ssimaexg  5449  dmfco  5455  fndmdif  5491  fmptco  5552  fliftf  5666  acexmidlem2  5737  acexmidlemv  5738  cbvoprab1  5809  cbvoprab2  5810  oprssdmm  6035  dmtpos  6119  tfrlemi1  6195  tfr1onlemaccex  6211  tfrcllemaccex  6224  ecdmn0m  6437  ereldm  6438  elqsn0m  6463  mapsn  6550  bren  6607  brdomg  6608  domeng  6612  ac6sfi  6758  ordiso  6887  ctssdclemr  6963  enumct  6966  ctssexmid  6990  exmidfodomrlemr  7022  exmidfodomrlemrALT  7023  acfun  7027  ccfunen  7043  recexnq  7162  prarloc  7275  genpdflem  7279  genpassl  7296  genpassu  7297  ltexprlemell  7370  ltexprlemelu  7371  ltexprlemm  7372  recexprlemell  7394  recexprlemelu  7395  cnm  7604  sup3exmid  8675  seq3f1olemp  10226  zfz1isolem1  10534  zfz1iso  10535  sumeq1  11075  sumeq2  11079  summodc  11103  fsum3  11107  fsum2dlemstep  11154  ctinf  11849  ctiunct  11859  bdsep2  12918  bdzfauscl  12922  strcoll2  13015  subctctexmid  13030  nninfall  13038
  Copyright terms: Public domain W3C validator