Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > breq1i | GIF version |
Description: Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) |
Ref | Expression |
---|---|
breq1i.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
breq1i | ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | breq1 3979 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 = wceq 1342 class class class wbr 3976 |
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 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-3an 969 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-v 2723 df-un 3115 df-sn 3576 df-pr 3577 df-op 3579 df-br 3977 |
This theorem is referenced by: eqbrtri 3997 brtpos0 6211 euen1 6759 euen1b 6760 2dom 6762 infglbti 6981 pr2nelem 7138 caucvgprprlemnbj 7625 caucvgprprlemmu 7627 caucvgprprlemaddq 7640 caucvgprprlem1 7641 gt0srpr 7680 caucvgsr 7734 mappsrprg 7736 map2psrprg 7737 pitonnlem1 7777 pitoregt0 7781 axprecex 7812 axpre-mulgt0 7819 axcaucvglemres 7831 lt0neg1 8357 le0neg1 8359 reclt1 8782 addltmul 9084 eluz2b1 9530 nn01to3 9546 xlt0neg1 9765 xle0neg1 9767 iccshftr 9921 iccshftl 9923 iccdil 9925 icccntr 9927 bernneq 10564 cbvsum 11287 expcnv 11431 cbvprod 11485 oddge22np1 11803 nn0o1gt2 11827 isprm3 12029 dvdsnprmd 12036 pw2dvdslemn 12076 txmetcnp 13065 sincosq1sgn 13294 sincosq3sgn 13296 sincosq4sgn 13297 logrpap0b 13344 |
Copyright terms: Public domain | W3C validator |