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

Theorem ralbidv 2326
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 1421 . 2  |-  F/ x ph
2 ralbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2ralbid 2324 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 98   A.wral 2306
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419
This theorem depends on definitions:  df-bi 110  df-nf 1350  df-ral 2311
This theorem is referenced by:  ralbii  2330  2ralbidv  2348  rexralbidv  2350  r19.32vdc  2459  raleqbi1dv  2513  raleqbidv  2517  cbvral2v  2541  rspc2  2661  rspc3v  2665  reu6i  2732  reu7  2736  sbcralt  2834  sbcralg  2836  raaanlem  3326  r19.12sn  3436  2ralunsn  3569  elintg  3623  elintrabg  3628  eliin  3662  bnd2  3926  poeq1  4036  soeq1  4052  frforeq1  4080  frforeq3  4084  frirrg  4087  frind  4089  weeq1  4093  reusv3  4192  ontr2exmid  4250  reg2exmidlema  4259  posng  4412  ralxpf  4482  cnvpom  4860  funcnvuni  4968  dff4im  5313  dff13f  5409  eusvobj2  5498  ofreq  5715  smoeq  5905  recseq  5921  tfr0  5937  tfrlemiex  5945  nneneq  6320  ac6sfi  6352  elinp  6570  prloc  6587  cauappcvgprlemladdru  6752  cauappcvgprlemladdrl  6753  caucvgpr  6778  caucvgprpr  6808  caucvgsrlemgt1  6877  caucvgsrlemoffres  6882  caucvgsr  6884  axcaucvglemcau  6970  axcaucvglemres  6971  nnsub  7950  indstr  8534  ublbneg  8546  lbzbi  8549  iccsupr  8833  cau4  9686  caubnd2  9687  clim  9776  clim2  9778  clim2c  9779  clim0c  9781  climabs0  9802  cn1lem  9808  sqrt2irr  9852  bj-omtrans  10055
  Copyright terms: Public domain W3C validator