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

Theorem ralbidv 2475
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 1526 . 2  |-  F/ x ph
2 ralbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2ralbid 2473 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105   A.wral 2453
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1445  ax-gen 1447  ax-4 1508  ax-17 1524
This theorem depends on definitions:  df-bi 117  df-nf 1459  df-ral 2458
This theorem is referenced by:  ralbii  2481  2ralbidv  2499  rexralbidv  2501  r19.32vdc  2624  raleqbi1dv  2678  raleqbidv  2682  cbvral2vw  2712  cbvral2v  2714  rspceaimv  2847  rspc2  2850  rspc3v  2855  reu6i  2926  reu7  2930  sbcralt  3037  sbcralg  3039  raaanlem  3526  2ralunsn  3794  elintg  3848  elintrabg  3853  eliin  3887  brralrspcev  4056  bnd2  4168  poeq1  4293  soeq1  4309  frforeq1  4337  frforeq3  4341  frirrg  4344  frind  4346  weeq1  4350  reusv3  4454  ontr2exmid  4518  reg2exmidlema  4527  posng  4692  ralxpf  4766  cnvpom  5163  funcnvuni  5277  fnmptfvd  5612  dff4im  5654  dff13f  5761  eusvobj2  5851  ovanraleqv  5889  ofreq  6076  smoeq  6281  recseq  6297  tfr0dm  6313  tfrlemiex  6322  tfr1onlemex  6338  tfr1onlemaccex  6339  tfrcllemsucaccv  6345  tfrcllembxssdm  6347  tfrcllemex  6351  tfrcllemaccex  6352  tfrcllemres  6353  elixp2  6692  xpf1o  6834  nneneq  6847  ac6sfi  6888  fimax2gtrilemstep  6890  fimax2gtri  6891  supeq1  6975  supeq3  6979  supmoti  6982  eqsupti  6985  supubti  6988  suplubti  6989  supisoex  6998  cnvinfex  7007  eqinfti  7009  infvalti  7011  updjud  7071  ctssdclemr  7101  nninff  7111  infnninf  7112  infnninfOLD  7113  nnnninf  7114  nnnninfeq  7116  nnnninfeq2  7117  enomnilem  7126  finomni  7128  exmidomni  7130  fodjuomnilemres  7136  ismkvnex  7143  fodjumkvlemres  7147  enmkvlem  7149  enwomnilem  7157  nninfdcinf  7159  nninfwlporlem  7161  nninfwlpoimlemg  7163  nninfwlpoimlemdc  7165  exmidontriimlem3  7212  exmidontriim  7214  cc2lem  7240  cc3  7242  elinp  7448  prloc  7465  cauappcvgprlemladdru  7630  cauappcvgprlemladdrl  7631  caucvgpr  7656  caucvgprpr  7686  suplocexprlemloc  7695  suplocexpr  7699  caucvgsrlemgt1  7769  caucvgsrlemoffres  7774  caucvgsr  7776  suplocsrlemb  7780  suplocsrlempr  7781  suplocsrlem  7782  axcaucvglemcau  7872  axcaucvglemres  7873  axpre-suploclemres  7875  axpre-suploc  7876  lbreu  8873  sup3exmid  8885  nnsub  8929  indstr  9564  supinfneg  9566  infsupneg  9567  ublbneg  9584  lbzbi  9587  iccsupr  9935  frecuzrdgsuc  10382  frecuzrdgg  10384  frecuzrdgsuctlem  10391  seq3f1olemstep  10469  seq3f1olemp  10470  nn0ltexp2  10656  bccl  10713  cau4  11092  caubnd2  11093  maxleast  11189  rexanre  11196  rexico  11197  fimaxre2  11202  minmax  11205  xrminmax  11240  clim  11256  clim2  11258  clim2c  11259  clim0c  11261  climabs0  11282  cn1lem  11289  sumeq1  11330  prodeq1f  11527  zsupcllemstep  11912  infssuzex  11916  suprzubdc  11919  nninfdcex  11920  zsupssdc  11921  bezoutlemstep  11964  bezoutlemmain  11965  bezoutlemex  11968  bezoutlemeu  11974  dfgcd3  11977  bezout  11978  dfgcd2  11981  nnwodc  12003  uzwodc  12004  nnwofdc  12005  sqrt2irr  12128  reumodprminv  12219  pc2dvds  12295  pcz  12297  prmpwdvds  12319  ennnfoneleminc  12378  ennnfonelemex  12381  ennnfonelemhom  12382  ennnfonelemnn0  12389  ennnfonelemr  12390  ennnfonelemim  12391  exmidunben  12393  ctinfomlemom  12394  ctinfom  12395  ctinf  12397  ctiunctlemudc  12404  ctiunct  12407  ssomct  12412  infpn2  12423  mgm1  12654  sgrp1  12681  mhmima  12736  dfgrp2  12762  isgrpinv  12786  grpidinv  12789  dfgrp3mlem  12827  srgideu  12948  basgen2  13074  bastop1  13076  iscn  13190  cnpval  13191  iscnp  13192  iscnp3  13196  cnprcl2k  13199  lmbr  13206  lmbr2  13207  lmbrf  13208  cnptoprest  13232  cnptoprest2  13233  cnmpt21  13284  ispsmet  13316  ismet  13337  isxmet  13338  metss  13487  qtopbasss  13514  cncfval  13552  elcncf2  13554  mulc1cncf  13569  cncfmet  13572  dedekindeulemloc  13590  dedekindeulemeu  13593  dedekindeu  13594  suplociccreex  13595  dedekindicclemloc  13599  dedekindicclemeu  13602  dedekindicclemicc  13603  ivthinclemlopn  13607  ivthinclemlr  13608  ivthinclemuopn  13609  ivthinclemur  13610  ivthinclemloc  13612  limccl  13621  ellimc3apf  13622  limcdifap  13624  limcmpted  13625  2irrexpqap  13889  2sqlem6  13949  2sqlem10  13954  bj-charfunbi  14045  bj-omtrans  14190  strcoll2  14217  strcollnfALT  14220  sscoll2  14222  pw1nct  14235  0nninf  14236  nnsf  14237  peano4nninf  14238  nninfalllem1  14240  nninfself  14245  nninfsellemeq  14246  nninfsellemeqinf  14248  isomninnlem  14261  trilpolemlt1  14272  iswomninnlem  14280  iswomni0  14282  ismkvnnlem  14283  dceqnconst  14290  dcapnconst  14291
  Copyright terms: Public domain W3C validator