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

Theorem ralbidv 2412
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 1491 . 2 𝑥𝜑
2 ralbidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2ralbid 2410 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wral 2391
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-4 1470  ax-17 1489
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-ral 2396
This theorem is referenced by:  ralbii  2416  2ralbidv  2434  rexralbidv  2436  r19.32vdc  2555  raleqbi1dv  2609  raleqbidv  2613  cbvral2v  2637  rspceaimv  2769  rspc2  2772  rspc3v  2777  reu6i  2846  reu7  2850  sbcralt  2955  sbcralg  2957  raaanlem  3436  2ralunsn  3693  elintg  3747  elintrabg  3752  eliin  3786  brralrspcev  3954  bnd2  4065  poeq1  4189  soeq1  4205  frforeq1  4233  frforeq3  4237  frirrg  4240  frind  4242  weeq1  4246  reusv3  4349  ontr2exmid  4408  reg2exmidlema  4417  posng  4579  ralxpf  4653  cnvpom  5049  funcnvuni  5160  dff4im  5532  dff13f  5637  eusvobj2  5726  ovanraleqv  5764  ofreq  5951  smoeq  6153  recseq  6169  tfr0dm  6185  tfrlemiex  6194  tfr1onlemex  6210  tfr1onlemaccex  6211  tfrcllemsucaccv  6217  tfrcllembxssdm  6219  tfrcllemex  6223  tfrcllemaccex  6224  tfrcllemres  6225  elixp2  6562  xpf1o  6704  nneneq  6717  ac6sfi  6758  fimax2gtrilemstep  6760  fimax2gtri  6761  supeq1  6839  supeq3  6843  supmoti  6846  eqsupti  6849  supubti  6852  suplubti  6853  supisoex  6862  cnvinfex  6871  eqinfti  6873  infvalti  6875  updjud  6933  ctssdclemr  6963  enomnilem  6976  finomni  6978  exmidomni  6980  fodjuomnilemres  6986  infnninf  6988  nnnninf  6989  ismkvnex  6995  fodjumkvlemres  6999  elinp  7246  prloc  7263  cauappcvgprlemladdru  7428  cauappcvgprlemladdrl  7429  caucvgpr  7454  caucvgprpr  7484  suplocexprlemloc  7493  suplocexpr  7497  caucvgsrlemgt1  7567  caucvgsrlemoffres  7572  caucvgsr  7574  suplocsrlemb  7578  suplocsrlempr  7579  suplocsrlem  7580  axcaucvglemcau  7670  axcaucvglemres  7671  axpre-suploclemres  7673  axpre-suploc  7674  lbreu  8660  sup3exmid  8672  nnsub  8716  indstr  9337  supinfneg  9339  infsupneg  9340  ublbneg  9354  lbzbi  9357  iccsupr  9689  frecuzrdgsuc  10127  frecuzrdgg  10129  frecuzrdgsuctlem  10136  seq3f1olemstep  10214  seq3f1olemp  10215  bccl  10453  cau4  10828  caubnd2  10829  maxleast  10925  rexanre  10932  rexico  10933  fimaxre2  10938  minmax  10941  xrminmax  10974  clim  10990  clim2  10992  clim2c  10993  clim0c  10995  climabs0  11016  cn1lem  11023  sumeq1  11064  zsupcllemstep  11534  infssuzex  11538  bezoutlemstep  11581  bezoutlemmain  11582  bezoutlemex  11585  bezoutlemeu  11591  dfgcd3  11594  bezout  11595  dfgcd2  11598  sqrt2irr  11736  ennnfoneleminc  11819  ennnfonelemex  11822  ennnfonelemhom  11823  ennnfonelemnn0  11830  ennnfonelemr  11831  ennnfonelemim  11832  exmidunben  11834  ctinfomlemom  11835  ctinfom  11836  ctinf  11838  ctiunctlemudc  11845  ctiunct  11848  basgen2  12145  bastop1  12147  iscn  12261  cnpval  12262  iscnp  12263  iscnp3  12267  cnprcl2k  12270  lmbr  12277  lmbr2  12278  lmbrf  12279  cnptoprest  12303  cnptoprest2  12304  cnmpt21  12355  ispsmet  12387  ismet  12408  isxmet  12409  metss  12558  qtopbasss  12585  cncfval  12623  elcncf2  12625  mulc1cncf  12640  cncfmet  12643  dedekindeulemloc  12661  dedekindeulemeu  12664  dedekindeu  12665  suplociccreex  12666  dedekindicclemloc  12670  dedekindicclemeu  12673  dedekindicc  12674  limccl  12680  ellimc3apf  12681  limcdifap  12683  limcmpted  12684  bj-omtrans  12965  0nninf  13008  nninff  13009  nnsf  13010  peano4nninf  13011  nninfalllemn  13013  nninfalllem1  13014  nninfself  13020  nninfsellemeq  13021  nninfsellemeqinf  13023  isomninnlem  13036  trilpolemlt1  13045
  Copyright terms: Public domain W3C validator