Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rneqd | GIF version |
Description: Equality deduction for range. (Contributed by NM, 4-Mar-2004.) |
Ref | Expression |
---|---|
rneqd.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
rneqd | ⊢ (𝜑 → ran 𝐴 = ran 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rneqd.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | rneq 4774 | . 2 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → ran 𝐴 = ran 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1332 ran crn 4548 |
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 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-3an 965 df-tru 1335 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-v 2691 df-un 3080 df-in 3082 df-ss 3089 df-sn 3538 df-pr 3539 df-op 3541 df-br 3938 df-opab 3998 df-cnv 4555 df-dm 4557 df-rn 4558 |
This theorem is referenced by: resima2 4861 imaeq1 4884 imaeq2 4885 resiima 4905 elxp4 5034 elxp5 5035 funimacnv 5207 funimaexg 5215 fnima 5249 fnrnfv 5476 2ndvalg 6049 fo2nd 6064 f2ndres 6066 en1 6701 xpassen 6732 xpdom2 6733 sbthlemi4 6856 djudom 6986 exmidfodomrlemim 7074 seqeq1 10252 seqeq2 10253 seqeq3 10254 seq3val 10262 seqvalcd 10263 ennnfonelemex 11963 ennnfonelemf1 11967 restval 12165 restid2 12168 tgrest 12377 txvalex 12462 txval 12463 mopnval 12650 |
Copyright terms: Public domain | W3C validator |