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

Theorem ralbidv 2438
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 1509 . 2  |-  F/ x ph
2 ralbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2ralbid 2436 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 2417
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 1424  ax-gen 1426  ax-4 1488  ax-17 1507
This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2422
This theorem is referenced by:  ralbii  2444  2ralbidv  2462  rexralbidv  2464  r19.32vdc  2583  raleqbi1dv  2637  raleqbidv  2641  cbvral2v  2668  rspceaimv  2800  rspc2  2803  rspc3v  2808  reu6i  2878  reu7  2882  sbcralt  2988  sbcralg  2990  raaanlem  3472  2ralunsn  3732  elintg  3786  elintrabg  3791  eliin  3825  brralrspcev  3993  bnd2  4104  poeq1  4228  soeq1  4244  frforeq1  4272  frforeq3  4276  frirrg  4279  frind  4281  weeq1  4285  reusv3  4388  ontr2exmid  4447  reg2exmidlema  4456  posng  4618  ralxpf  4692  cnvpom  5088  funcnvuni  5199  dff4im  5573  dff13f  5678  eusvobj2  5767  ovanraleqv  5805  ofreq  5992  smoeq  6194  recseq  6210  tfr0dm  6226  tfrlemiex  6235  tfr1onlemex  6251  tfr1onlemaccex  6252  tfrcllemsucaccv  6258  tfrcllembxssdm  6260  tfrcllemex  6264  tfrcllemaccex  6265  tfrcllemres  6266  elixp2  6603  xpf1o  6745  nneneq  6758  ac6sfi  6799  fimax2gtrilemstep  6801  fimax2gtri  6802  supeq1  6880  supeq3  6884  supmoti  6887  eqsupti  6890  supubti  6893  suplubti  6894  supisoex  6903  cnvinfex  6912  eqinfti  6914  infvalti  6916  updjud  6974  ctssdclemr  7004  enomnilem  7017  finomni  7019  exmidomni  7021  fodjuomnilemres  7027  infnninf  7029  nnnninf  7030  ismkvnex  7036  fodjumkvlemres  7040  enmkvlem  7042  enwomnilem  7049  cc2lem  7097  cc3  7099  elinp  7305  prloc  7322  cauappcvgprlemladdru  7487  cauappcvgprlemladdrl  7488  caucvgpr  7513  caucvgprpr  7543  suplocexprlemloc  7552  suplocexpr  7556  caucvgsrlemgt1  7626  caucvgsrlemoffres  7631  caucvgsr  7633  suplocsrlemb  7637  suplocsrlempr  7638  suplocsrlem  7639  axcaucvglemcau  7729  axcaucvglemres  7730  axpre-suploclemres  7732  axpre-suploc  7733  lbreu  8726  sup3exmid  8738  nnsub  8782  indstr  9414  supinfneg  9416  infsupneg  9417  ublbneg  9431  lbzbi  9434  iccsupr  9778  frecuzrdgsuc  10217  frecuzrdgg  10219  frecuzrdgsuctlem  10226  seq3f1olemstep  10304  seq3f1olemp  10305  bccl  10544  cau4  10919  caubnd2  10920  maxleast  11016  rexanre  11023  rexico  11024  fimaxre2  11029  minmax  11032  xrminmax  11065  clim  11081  clim2  11083  clim2c  11084  clim0c  11086  climabs0  11107  cn1lem  11114  sumeq1  11155  prodeq1f  11352  zsupcllemstep  11672  infssuzex  11676  bezoutlemstep  11719  bezoutlemmain  11720  bezoutlemex  11723  bezoutlemeu  11729  dfgcd3  11732  bezout  11733  dfgcd2  11736  sqrt2irr  11874  ennnfoneleminc  11958  ennnfonelemex  11961  ennnfonelemhom  11962  ennnfonelemnn0  11969  ennnfonelemr  11970  ennnfonelemim  11971  exmidunben  11973  ctinfomlemom  11974  ctinfom  11975  ctinf  11977  ctiunctlemudc  11984  ctiunct  11987  basgen2  12287  bastop1  12289  iscn  12403  cnpval  12404  iscnp  12405  iscnp3  12409  cnprcl2k  12412  lmbr  12419  lmbr2  12420  lmbrf  12421  cnptoprest  12445  cnptoprest2  12446  cnmpt21  12497  ispsmet  12529  ismet  12550  isxmet  12551  metss  12700  qtopbasss  12727  cncfval  12765  elcncf2  12767  mulc1cncf  12782  cncfmet  12785  dedekindeulemloc  12803  dedekindeulemeu  12806  dedekindeu  12807  suplociccreex  12808  dedekindicclemloc  12812  dedekindicclemeu  12815  dedekindicclemicc  12816  ivthinclemlopn  12820  ivthinclemlr  12821  ivthinclemuopn  12822  ivthinclemur  12823  ivthinclemloc  12825  limccl  12834  ellimc3apf  12835  limcdifap  12837  limcmpted  12838  2irrexpqap  13101  bj-omtrans  13323  strcoll2  13350  strcollnfALT  13353  sscoll2  13355  pw1nct  13369  0nninf  13370  nninff  13371  nnsf  13372  peano4nninf  13373  nninfalllemn  13375  nninfalllem1  13376  nninfself  13382  nninfsellemeq  13383  nninfsellemeqinf  13385  isomninnlem  13398  trilpolemlt1  13407  iswomninnlem  13415  ismkvnnlem  13417  dcapncf  13421
  Copyright terms: Public domain W3C validator