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

Theorem ralbidv 2343
Description: Formula-building rule for restricted universal quantifier (deduction rule). (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 1437 . 2  |-  F/ x ph
2 ralbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2ralbid 2341 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102   A.wral 2323
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-4 1416  ax-17 1435
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-ral 2328
This theorem is referenced by:  ralbii  2347  2ralbidv  2365  rexralbidv  2367  r19.32vdc  2476  raleqbi1dv  2530  raleqbidv  2534  cbvral2v  2558  rspc2  2683  rspc3v  2688  reu6i  2755  reu7  2759  sbcralt  2862  sbcralg  2864  raaanlem  3354  r19.12sn  3464  2ralunsn  3597  elintg  3651  elintrabg  3656  eliin  3690  bnd2  3954  poeq1  4064  soeq1  4080  frforeq1  4108  frforeq3  4112  frirrg  4115  frind  4117  weeq1  4121  reusv3  4220  ontr2exmid  4278  reg2exmidlema  4287  posng  4440  ralxpf  4510  cnvpom  4888  funcnvuni  4996  dff4im  5341  dff13f  5437  eusvobj2  5526  ofreq  5743  smoeq  5936  recseq  5952  tfr0  5968  tfrlemiex  5976  nneneq  6351  ac6sfi  6383  supeq1  6392  supeq3  6396  supmoti  6399  eqsupti  6402  supubti  6405  suplubti  6406  supisoex  6413  elinp  6630  prloc  6647  cauappcvgprlemladdru  6812  cauappcvgprlemladdrl  6813  caucvgpr  6838  caucvgprpr  6868  caucvgsrlemgt1  6937  caucvgsrlemoffres  6942  caucvgsr  6944  axcaucvglemcau  7030  axcaucvglemres  7031  nnsub  8028  indstr  8632  ublbneg  8645  lbzbi  8648  iccsupr  8936  bccl  9635  cau4  9943  caubnd2  9944  clim  10033  clim2  10035  clim2c  10036  clim0c  10038  climabs0  10059  cn1lem  10065  sqrt2irr  10251  bj-omtrans  10468
  Copyright terms: Public domain W3C validator