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

Theorem rabbiia 2694
 Description: Equivalent wff's yield equal restricted class abstractions (inference form). (Contributed by NM, 22-May-1999.)
Hypothesis
Ref Expression
rabbiia.1
Assertion
Ref Expression
rabbiia

Proof of Theorem rabbiia
StepHypRef Expression
1 rabbiia.1 . . . 4
21pm5.32i 450 . . 3
32abbii 2270 . 2
4 df-rab 2441 . 2
5 df-rab 2441 . 2
63, 4, 53eqtr4i 2185 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104   wceq 1332   wcel 2125  cab 2140  crab 2436 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-11 1483  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-ext 2136 This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1740  df-clab 2141  df-cleq 2147  df-rab 2441 This theorem is referenced by:  rabbii  2695  bm2.5ii  4449  fndmdifcom  5566  cauappcvgprlemladdru  7555  cauappcvgprlemladdrl  7556  cauappcvgpr  7561  caucvgprlemcl  7575  caucvgprlemladdrl  7577  caucvgpr  7581  caucvgprprlemclphr  7604  ioopos  9832  gcdcom  11829  gcdass  11870  lcmcom  11912  lcmass  11933
 Copyright terms: Public domain W3C validator