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

Theorem 2ralbidv 2501
Description: Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.)
Hypothesis
Ref Expression
2ralbidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
2ralbidv  |-  ( ph  ->  ( A. x  e.  A  A. y  e.  B  ps  <->  A. x  e.  A  A. y  e.  B  ch )
)
Distinct variable groups:    ph, x    ph, y
Allowed substitution hints:    ps( x, y)    ch( x, y)    A( x, y)    B( x, y)

Proof of Theorem 2ralbidv
StepHypRef Expression
1 2ralbidv.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21ralbidv 2477 . 2  |-  ( ph  ->  ( A. y  e.  B  ps  <->  A. y  e.  B  ch )
)
32ralbidv 2477 1  |-  ( ph  ->  ( A. x  e.  A  A. y  e.  B  ps  <->  A. x  e.  A  A. y  e.  B  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105   A.wral 2455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460
This theorem is referenced by:  cbvral3v  2720  poeq1  4301  soeq1  4317  isoeq1  5805  isoeq2  5806  isoeq3  5807  fnmpoovd  6219  smoeq  6294  xpf1o  6847  tapeq1  7254  elinp  7476  cauappcvgpr  7664  seq3caopr2  10485  addcn2  11321  mulcn2  11323  sgrp1  12823  ismhm  12861  issubm  12871  isnsg  13076  nmznsg  13087  iscmn  13111  ring1  13274  issubrg3  13406  islmod  13419  lmodlema  13420  lsssetm  13482  islssmd  13484  ispsmet  14011  ismet  14032  isxmet  14033  addcncntoplem  14239  elcncf  14248
  Copyright terms: Public domain W3C validator