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

Theorem rabeq 2652
Description: Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.)
Assertion
Ref Expression
rabeq  |-  ( A  =  B  ->  { x  e.  A  |  ph }  =  { x  e.  B  |  ph } )
Distinct variable groups:    x, A    x, B
Allowed substitution hint:    ph( x)

Proof of Theorem rabeq
StepHypRef Expression
1 nfcv 2258 . 2  |-  F/_ x A
2 nfcv 2258 . 2  |-  F/_ x B
31, 2rabeqf 2650 1  |-  ( A  =  B  ->  { x  e.  A  |  ph }  =  { x  e.  B  |  ph } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1316   {crab 2397
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-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-rab 2402
This theorem is referenced by:  rabeqdv  2654  rabeqbidv  2655  rabeqbidva  2656  difeq1  3157  ifeq1  3447  ifeq2  3448  elfvmptrab  5484  pmvalg  6521  unfiexmid  6774  ssfirab  6790  supeq2  6844  iooval2  9666  fzval2  9761  lcmval  11671  lcmcllem  11675  lcmledvds  11678  clsfval  12197
  Copyright terms: Public domain W3C validator