![]() |
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 4022 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 = wceq 1364 class class class wbr 4018 |
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 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-v 2754 df-un 3148 df-sn 3613 df-pr 3614 df-op 3616 df-br 4019 |
This theorem is referenced by: breqtri 4043 en1 6824 snnen2og 6886 1nen2 6888 pm54.43 7218 caucvgprprlemval 7716 caucvgprprlemmu 7723 caucvgsr 7830 pitonnlem1 7873 lt0neg2 8455 le0neg2 8457 negap0 8616 recexaplem2 8638 recgt1 8883 crap0 8944 addltmul 9184 nn0lt10b 9362 nn0lt2 9363 3halfnz 9379 xlt0neg2 9868 xle0neg2 9870 iccshftr 10023 iccshftl 10025 iccdil 10027 icccntr 10029 fihashen1 10810 cjap0 10947 abs00ap 11102 xrmaxiflemval 11289 mertenslem2 11575 mertensabs 11576 3dvdsdec 11901 3dvds2dec 11902 ndvdsi 11969 3prm 12159 prmfac1 12183 prm23lt5 12294 sinhalfpilem 14664 sincosq1lem 14698 sincosq1sgn 14699 sincosq2sgn 14700 sincosq3sgn 14701 sincosq4sgn 14702 logrpap0b 14749 2lgsoddprmlem3 14912 |
Copyright terms: Public domain | W3C validator |