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

Theorem breq2i 4008
Description: Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
Hypothesis
Ref Expression
breq1i.1  |-  A  =  B
Assertion
Ref Expression
breq2i  |-  ( C R A  <->  C R B )

Proof of Theorem breq2i
StepHypRef Expression
1 breq1i.1 . 2  |-  A  =  B
2 breq2 4004 . 2  |-  ( A  =  B  ->  ( C R A  <->  C R B ) )
31, 2ax-mp 5 1  |-  ( C R A  <->  C R B )
Colors of variables: wff set class
Syntax hints:    <-> wb 105    = wceq 1353   class class class wbr 4000
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-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-sn 3597  df-pr 3598  df-op 3600  df-br 4001
This theorem is referenced by:  breqtri  4025  en1  6792  snnen2og  6852  1nen2  6854  pm54.43  7182  caucvgprprlemval  7665  caucvgprprlemmu  7672  caucvgsr  7779  pitonnlem1  7822  lt0neg2  8403  le0neg2  8405  negap0  8564  recexaplem2  8585  recgt1  8830  crap0  8891  addltmul  9131  nn0lt10b  9309  nn0lt2  9310  3halfnz  9326  xlt0neg2  9813  xle0neg2  9815  iccshftr  9968  iccshftl  9970  iccdil  9972  icccntr  9974  fihashen1  10750  cjap0  10887  abs00ap  11042  xrmaxiflemval  11229  mertenslem2  11515  mertensabs  11516  3dvdsdec  11840  3dvds2dec  11841  ndvdsi  11908  3prm  12098  prmfac1  12122  prm23lt5  12233  sinhalfpilem  13845  sincosq1lem  13879  sincosq1sgn  13880  sincosq2sgn  13881  sincosq3sgn  13882  sincosq4sgn  13883  logrpap0b  13930
  Copyright terms: Public domain W3C validator