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

Theorem ralbidv 2414
Description: Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 20-Nov-1994.)
Hypothesis
Ref Expression
ralbidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
ralbidv  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  A  ch )
)
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)

Proof of Theorem ralbidv
StepHypRef Expression
1 nfv 1493 . 2  |-  F/ x ph
2 ralbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2ralbid 2412 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104   A.wral 2393
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-4 1472  ax-17 1491
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-ral 2398
This theorem is referenced by:  ralbii  2418  2ralbidv  2436  rexralbidv  2438  r19.32vdc  2557  raleqbi1dv  2611  raleqbidv  2615  cbvral2v  2639  rspceaimv  2771  rspc2  2774  rspc3v  2779  reu6i  2848  reu7  2852  sbcralt  2957  sbcralg  2959  raaanlem  3438  2ralunsn  3695  elintg  3749  elintrabg  3754  eliin  3788  brralrspcev  3956  bnd2  4067  poeq1  4191  soeq1  4207  frforeq1  4235  frforeq3  4239  frirrg  4242  frind  4244  weeq1  4248  reusv3  4351  ontr2exmid  4410  reg2exmidlema  4419  posng  4581  ralxpf  4655  cnvpom  5051  funcnvuni  5162  dff4im  5534  dff13f  5639  eusvobj2  5728  ovanraleqv  5766  ofreq  5953  smoeq  6155  recseq  6171  tfr0dm  6187  tfrlemiex  6196  tfr1onlemex  6212  tfr1onlemaccex  6213  tfrcllemsucaccv  6219  tfrcllembxssdm  6221  tfrcllemex  6225  tfrcllemaccex  6226  tfrcllemres  6227  elixp2  6564  xpf1o  6706  nneneq  6719  ac6sfi  6760  fimax2gtrilemstep  6762  fimax2gtri  6763  supeq1  6841  supeq3  6845  supmoti  6848  eqsupti  6851  supubti  6854  suplubti  6855  supisoex  6864  cnvinfex  6873  eqinfti  6875  infvalti  6877  updjud  6935  ctssdclemr  6965  enomnilem  6978  finomni  6980  exmidomni  6982  fodjuomnilemres  6988  infnninf  6990  nnnninf  6991  ismkvnex  6997  fodjumkvlemres  7001  elinp  7250  prloc  7267  cauappcvgprlemladdru  7432  cauappcvgprlemladdrl  7433  caucvgpr  7458  caucvgprpr  7488  suplocexprlemloc  7497  suplocexpr  7501  caucvgsrlemgt1  7571  caucvgsrlemoffres  7576  caucvgsr  7578  suplocsrlemb  7582  suplocsrlempr  7583  suplocsrlem  7584  axcaucvglemcau  7674  axcaucvglemres  7675  axpre-suploclemres  7677  axpre-suploc  7678  lbreu  8671  sup3exmid  8683  nnsub  8727  indstr  9356  supinfneg  9358  infsupneg  9359  ublbneg  9373  lbzbi  9376  iccsupr  9717  frecuzrdgsuc  10155  frecuzrdgg  10157  frecuzrdgsuctlem  10164  seq3f1olemstep  10242  seq3f1olemp  10243  bccl  10481  cau4  10856  caubnd2  10857  maxleast  10953  rexanre  10960  rexico  10961  fimaxre2  10966  minmax  10969  xrminmax  11002  clim  11018  clim2  11020  clim2c  11021  clim0c  11023  climabs0  11044  cn1lem  11051  sumeq1  11092  zsupcllemstep  11565  infssuzex  11569  bezoutlemstep  11612  bezoutlemmain  11613  bezoutlemex  11616  bezoutlemeu  11622  dfgcd3  11625  bezout  11626  dfgcd2  11629  sqrt2irr  11767  ennnfoneleminc  11851  ennnfonelemex  11854  ennnfonelemhom  11855  ennnfonelemnn0  11862  ennnfonelemr  11863  ennnfonelemim  11864  exmidunben  11866  ctinfomlemom  11867  ctinfom  11868  ctinf  11870  ctiunctlemudc  11877  ctiunct  11880  basgen2  12177  bastop1  12179  iscn  12293  cnpval  12294  iscnp  12295  iscnp3  12299  cnprcl2k  12302  lmbr  12309  lmbr2  12310  lmbrf  12311  cnptoprest  12335  cnptoprest2  12336  cnmpt21  12387  ispsmet  12419  ismet  12440  isxmet  12441  metss  12590  qtopbasss  12617  cncfval  12655  elcncf2  12657  mulc1cncf  12672  cncfmet  12675  dedekindeulemloc  12693  dedekindeulemeu  12696  dedekindeu  12697  suplociccreex  12698  dedekindicclemloc  12702  dedekindicclemeu  12705  dedekindicclemicc  12706  ivthinclemlopn  12710  ivthinclemlr  12711  ivthinclemuopn  12712  ivthinclemur  12713  ivthinclemloc  12715  limccl  12724  ellimc3apf  12725  limcdifap  12727  limcmpted  12728  bj-omtrans  13081  0nninf  13124  nninff  13125  nnsf  13126  peano4nninf  13127  nninfalllemn  13129  nninfalllem1  13130  nninfself  13136  nninfsellemeq  13137  nninfsellemeqinf  13139  isomninnlem  13152  trilpolemlt1  13161
  Copyright terms: Public domain W3C validator