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

Theorem ralbidv 2376
Description: Formula-building rule for restricted universal quantifier (deduction rule). (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 1464 . 2 𝑥𝜑
2 ralbidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2ralbid 2374 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103  wral 2355
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-4 1443  ax-17 1462
This theorem depends on definitions:  df-bi 115  df-nf 1393  df-ral 2360
This theorem is referenced by:  ralbii  2380  2ralbidv  2398  rexralbidv  2400  r19.32vdc  2512  raleqbi1dv  2566  raleqbidv  2570  cbvral2v  2594  rspc2  2724  rspc3v  2729  reu6i  2797  reu7  2801  sbcralt  2904  sbcralg  2906  raaanlem  3374  2ralunsn  3627  elintg  3681  elintrabg  3686  eliin  3720  bnd2  3985  poeq1  4102  soeq1  4118  frforeq1  4146  frforeq3  4150  frirrg  4153  frind  4155  weeq1  4159  reusv3  4258  ontr2exmid  4316  reg2exmidlema  4325  posng  4480  ralxpf  4552  cnvpom  4941  funcnvuni  5050  dff4im  5410  dff13f  5512  eusvobj2  5601  ofreq  5818  smoeq  6011  recseq  6027  tfr0dm  6043  tfrlemiex  6052  tfr1onlemex  6068  tfr1onlemaccex  6069  tfrcllemsucaccv  6075  tfrcllembxssdm  6077  tfrcllemex  6081  tfrcllemaccex  6082  tfrcllemres  6083  xpf1o  6514  nneneq  6527  ac6sfi  6568  fimax2gtrilemstep  6570  fimax2gtri  6571  supeq1  6628  supeq3  6632  supmoti  6635  eqsupti  6638  supubti  6641  suplubti  6642  supisoex  6651  cnvinfex  6660  eqinfti  6662  infvalti  6664  updjud  6720  enomnilem  6741  finomni  6743  exmidomni  6745  fodjuomnilemres  6750  infnninf  6752  nnnninf  6753  elinp  6980  prloc  6997  cauappcvgprlemladdru  7162  cauappcvgprlemladdrl  7163  caucvgpr  7188  caucvgprpr  7218  caucvgsrlemgt1  7287  caucvgsrlemoffres  7292  caucvgsr  7294  axcaucvglemcau  7380  axcaucvglemres  7381  lbreu  8344  nnsub  8398  indstr  9016  supinfneg  9018  infsupneg  9019  ublbneg  9033  lbzbi  9036  iccsupr  9319  frecuzrdgsuc  9752  frecuzrdgg  9754  frecuzrdgsuctlem  9761  iseqf1olemstep  9838  iseqf1olemp  9839  bccl  10075  cau4  10448  caubnd2  10449  maxleast  10545  rexanre  10552  rexico  10553  fimaxre2  10556  minmax  10559  clim  10567  clim2  10569  clim2c  10570  clim0c  10572  climabs0  10593  cn1lem  10599  sumeq1  10639  zsupcllemstep  10847  infssuzex  10851  bezoutlemstep  10892  bezoutlemmain  10893  bezoutlemex  10896  bezoutlemeu  10902  dfgcd3  10905  bezout  10906  dfgcd2  10909  sqrt2irr  11047  bj-omtrans  11320  0nninf  11362  nninff  11363  nnsf  11364  peano4nninf  11365  nninfalllemn  11367  nninfalllem1  11368  nninfself  11374  nninfsellemeq  11375  nninfsellemeqinf  11377
  Copyright terms: Public domain W3C validator