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

Theorem ralbidv 2369
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 1462 . 2 𝑥𝜑
2 ralbidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2ralbid 2367 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103  wral 2349
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 1377  ax-gen 1379  ax-4 1441  ax-17 1460
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-ral 2354
This theorem is referenced by:  ralbii  2373  2ralbidv  2391  rexralbidv  2393  r19.32vdc  2504  raleqbi1dv  2558  raleqbidv  2562  cbvral2v  2586  rspc2  2712  rspc3v  2717  reu6i  2784  reu7  2788  sbcralt  2891  sbcralg  2893  raaanlem  3354  2ralunsn  3598  elintg  3652  elintrabg  3657  eliin  3691  bnd2  3955  poeq1  4062  soeq1  4078  frforeq1  4106  frforeq3  4110  frirrg  4113  frind  4115  weeq1  4119  reusv3  4218  ontr2exmid  4276  reg2exmidlema  4285  posng  4438  ralxpf  4510  cnvpom  4890  funcnvuni  4999  dff4im  5345  dff13f  5441  eusvobj2  5529  ofreq  5746  smoeq  5939  recseq  5955  tfr0dm  5971  tfrlemiex  5980  tfr1onlemex  5996  tfr1onlemaccex  5997  tfrcllemsucaccv  6003  tfrcllembxssdm  6005  tfrcllemex  6009  tfrcllemaccex  6010  tfrcllemres  6011  xpf1o  6385  nneneq  6392  ac6sfi  6431  supeq1  6458  supeq3  6462  supmoti  6465  eqsupti  6468  supubti  6471  suplubti  6472  supisoex  6481  cnvinfex  6490  eqinfti  6492  infvalti  6494  elinp  6726  prloc  6743  cauappcvgprlemladdru  6908  cauappcvgprlemladdrl  6909  caucvgpr  6934  caucvgprpr  6964  caucvgsrlemgt1  7033  caucvgsrlemoffres  7038  caucvgsr  7040  axcaucvglemcau  7126  axcaucvglemres  7127  lbreu  8090  nnsub  8144  indstr  8762  supinfneg  8764  infsupneg  8765  ublbneg  8779  lbzbi  8782  iccsupr  9065  frecuzrdgsuc  9496  frecuzrdgg  9498  frecuzrdgsuctlem  9505  bccl  9791  cau4  10140  caubnd2  10141  maxleast  10237  rexanre  10244  rexico  10245  fimaxre2  10247  minmax  10250  clim  10258  clim2  10260  clim2c  10261  clim0c  10263  climabs0  10284  cn1lem  10290  sumeq1  10330  zsupcllemstep  10485  infssuzex  10489  bezoutlemstep  10530  bezoutlemmain  10531  bezoutlemex  10534  bezoutlemeu  10540  dfgcd3  10543  bezout  10544  dfgcd2  10547  sqrt2irr  10685  bj-omtrans  10909
  Copyright terms: Public domain W3C validator