![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > breq2i | GIF version |
Description: Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) |
Ref | Expression |
---|---|
breq1i.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
breq2i | ⊢ (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | breq2 3871 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵)) | |
3 | 1, 2 | ax-mp 7 | 1 ⊢ (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 = wceq 1296 class class class wbr 3867 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-3an 929 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-v 2635 df-un 3017 df-sn 3472 df-pr 3473 df-op 3475 df-br 3868 |
This theorem is referenced by: breqtri 3890 en1 6596 snnen2og 6655 1nen2 6657 pm54.43 6915 caucvgprprlemval 7344 caucvgprprlemmu 7351 caucvgsr 7444 pitonnlem1 7479 lt0neg2 8044 le0neg2 8046 negap0 8203 recexaplem2 8218 recgt1 8455 crap0 8516 addltmul 8750 nn0lt10b 8925 nn0lt2 8926 3halfnz 8942 xlt0neg2 9405 xle0neg2 9407 iccshftr 9560 iccshftl 9562 iccdil 9564 icccntr 9566 fihashen1 10322 cjap0 10456 abs00ap 10610 xrmaxiflemval 10793 mertenslem2 11079 mertensabs 11080 3dvdsdec 11292 3dvds2dec 11293 ndvdsi 11360 3prm 11537 prmfac1 11558 |
Copyright terms: Public domain | W3C validator |