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

Theorem ralbidv 2477
Description: Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 20-Nov-1994.)
Hypothesis
Ref Expression
ralbidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
ralbidv (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ralbidv
StepHypRef Expression
1 nfv 1528 . 2 𝑥𝜑
2 ralbidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2ralbid 2475 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105  wral 2455
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 1447  ax-gen 1449  ax-4 1510  ax-17 1526
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460
This theorem is referenced by:  ralbii  2483  2ralbidv  2501  rexralbidv  2503  r19.32vdc  2626  raleqbi1dv  2680  raleqbidv  2684  cbvral2vw  2714  cbvral2v  2716  rspceaimv  2849  rspc2  2852  rspc3v  2857  reu6i  2928  reu7  2932  sbcralt  3039  sbcralg  3041  raaanlem  3528  2ralunsn  3796  elintg  3850  elintrabg  3855  eliin  3889  brralrspcev  4058  bnd2  4170  poeq1  4296  soeq1  4312  frforeq1  4340  frforeq3  4344  frirrg  4347  frind  4349  weeq1  4353  reusv3  4457  ontr2exmid  4521  reg2exmidlema  4530  posng  4695  ralxpf  4769  cnvpom  5167  funcnvuni  5281  fnmptfvd  5616  dff4im  5658  dff13f  5765  eusvobj2  5855  ovanraleqv  5893  ofreq  6080  smoeq  6285  recseq  6301  tfr0dm  6317  tfrlemiex  6326  tfr1onlemex  6342  tfr1onlemaccex  6343  tfrcllemsucaccv  6349  tfrcllembxssdm  6351  tfrcllemex  6355  tfrcllemaccex  6356  tfrcllemres  6357  elixp2  6696  xpf1o  6838  nneneq  6851  ac6sfi  6892  fimax2gtrilemstep  6894  fimax2gtri  6895  supeq1  6979  supeq3  6983  supmoti  6986  eqsupti  6989  supubti  6992  suplubti  6993  supisoex  7002  cnvinfex  7011  eqinfti  7013  infvalti  7015  updjud  7075  ctssdclemr  7105  nninff  7115  infnninf  7116  infnninfOLD  7117  nnnninf  7118  nnnninfeq  7120  nnnninfeq2  7121  enomnilem  7130  finomni  7132  exmidomni  7134  fodjuomnilemres  7140  ismkvnex  7147  fodjumkvlemres  7151  enmkvlem  7153  enwomnilem  7161  nninfdcinf  7163  nninfwlporlem  7165  nninfwlpoimlemg  7167  nninfwlpoimlemdc  7169  exmidontriimlem3  7216  exmidontriim  7218  tapeq1  7242  netap  7243  cc2lem  7253  cc3  7255  elinp  7461  prloc  7478  cauappcvgprlemladdru  7643  cauappcvgprlemladdrl  7644  caucvgpr  7669  caucvgprpr  7699  suplocexprlemloc  7708  suplocexpr  7712  caucvgsrlemgt1  7782  caucvgsrlemoffres  7787  caucvgsr  7789  suplocsrlemb  7793  suplocsrlempr  7794  suplocsrlem  7795  axcaucvglemcau  7885  axcaucvglemres  7886  axpre-suploclemres  7888  axpre-suploc  7889  lbreu  8888  sup3exmid  8900  nnsub  8944  indstr  9579  supinfneg  9581  infsupneg  9582  ublbneg  9599  lbzbi  9602  iccsupr  9950  frecuzrdgsuc  10397  frecuzrdgg  10399  frecuzrdgsuctlem  10406  seq3f1olemstep  10484  seq3f1olemp  10485  nn0ltexp2  10671  bccl  10728  cau4  11106  caubnd2  11107  maxleast  11203  rexanre  11210  rexico  11211  fimaxre2  11216  minmax  11219  xrminmax  11254  clim  11270  clim2  11272  clim2c  11273  clim0c  11275  climabs0  11296  cn1lem  11303  sumeq1  11344  prodeq1f  11541  zsupcllemstep  11926  infssuzex  11930  suprzubdc  11933  nninfdcex  11934  zsupssdc  11935  bezoutlemstep  11978  bezoutlemmain  11979  bezoutlemex  11982  bezoutlemeu  11988  dfgcd3  11991  bezout  11992  dfgcd2  11995  nnwodc  12017  uzwodc  12018  nnwofdc  12019  sqrt2irr  12142  reumodprminv  12233  pc2dvds  12309  pcz  12311  prmpwdvds  12333  ennnfoneleminc  12392  ennnfonelemex  12395  ennnfonelemhom  12396  ennnfonelemnn0  12403  ennnfonelemr  12404  ennnfonelemim  12405  exmidunben  12407  ctinfomlemom  12408  ctinfom  12409  ctinf  12411  ctiunctlemudc  12418  ctiunct  12421  ssomct  12426  infpn2  12437  mgm1  12678  sgrp1  12705  mhmima  12762  dfgrp2  12789  isgrpinv  12813  grpidinv  12816  dfgrp3mlem  12854  srgideu  12978  ring1  13059  basgen2  13241  bastop1  13243  iscn  13357  cnpval  13358  iscnp  13359  iscnp3  13363  cnprcl2k  13366  lmbr  13373  lmbr2  13374  lmbrf  13375  cnptoprest  13399  cnptoprest2  13400  cnmpt21  13451  ispsmet  13483  ismet  13504  isxmet  13505  metss  13654  qtopbasss  13681  cncfval  13719  elcncf2  13721  mulc1cncf  13736  cncfmet  13739  dedekindeulemloc  13757  dedekindeulemeu  13760  dedekindeu  13761  suplociccreex  13762  dedekindicclemloc  13766  dedekindicclemeu  13769  dedekindicclemicc  13770  ivthinclemlopn  13774  ivthinclemlr  13775  ivthinclemuopn  13776  ivthinclemur  13777  ivthinclemloc  13779  limccl  13788  ellimc3apf  13789  limcdifap  13791  limcmpted  13792  2irrexpqap  14056  2sqlem6  14116  2sqlem10  14121  bj-charfunbi  14212  bj-omtrans  14357  strcoll2  14384  strcollnfALT  14387  sscoll2  14389  pw1nct  14401  0nninf  14402  nnsf  14403  peano4nninf  14404  nninfalllem1  14406  nninfself  14411  nninfsellemeq  14412  nninfsellemeqinf  14414  isomninnlem  14427  trilpolemlt1  14438  iswomninnlem  14446  iswomni0  14448  ismkvnnlem  14449  dceqnconst  14456  dcapnconst  14457
  Copyright terms: Public domain W3C validator