![]() |
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 3791 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵)) | |
3 | 1, 2 | ax-mp 7 | 1 ⊢ (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 103 = wceq 1285 class class class wbr 3787 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2064 |
This theorem depends on definitions: df-bi 115 df-3an 922 df-tru 1288 df-nf 1391 df-sb 1687 df-clab 2069 df-cleq 2075 df-clel 2078 df-nfc 2209 df-v 2604 df-un 2978 df-sn 3406 df-pr 3407 df-op 3409 df-br 3788 |
This theorem is referenced by: breqtri 3810 en1 6338 snnen2og 6384 1nen2 6386 pm54.43 6508 caucvgprprlemval 6929 caucvgprprlemmu 6936 caucvgsr 7029 pitonnlem1 7064 lt0neg2 7629 le0neg2 7631 negap0 7785 recexaplem2 7798 recgt1 8031 crap0 8091 addltmul 8323 nn0lt10b 8498 nn0lt2 8499 3halfnz 8514 xlt0neg2 8971 xle0neg2 8973 iccshftr 9081 iccshftl 9083 iccdil 9085 icccntr 9087 sizeen1 9812 cjap0 9921 abs00ap 10075 3dvdsdec 10398 3dvds2dec 10399 ndvdsi 10466 3prm 10643 prmfac1 10664 |
Copyright terms: Public domain | W3C validator |