![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > predeq3 | Structured version Visualization version GIF version |
Description: Equality theorem for the predecessor class. (Contributed by Scott Fenton, 2-Feb-2011.) |
Ref | Expression |
---|---|
predeq3 | ⊢ (𝑋 = 𝑌 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2772 | . 2 ⊢ 𝑅 = 𝑅 | |
2 | eqid 2772 | . 2 ⊢ 𝐴 = 𝐴 | |
3 | predeq123 5981 | . 2 ⊢ ((𝑅 = 𝑅 ∧ 𝐴 = 𝐴 ∧ 𝑋 = 𝑌) → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌)) | |
4 | 1, 2, 3 | mp3an12 1430 | 1 ⊢ (𝑋 = 𝑌 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1507 Predcpred 5979 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-ext 2745 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-clab 2754 df-cleq 2765 df-clel 2840 df-nfc 2912 df-rab 3091 df-v 3411 df-dif 3828 df-un 3830 df-in 3832 df-ss 3839 df-nul 4174 df-if 4345 df-sn 4436 df-pr 4438 df-op 4442 df-br 4924 df-opab 4986 df-xp 5406 df-cnv 5408 df-dm 5410 df-rn 5411 df-res 5412 df-ima 5413 df-pred 5980 |
This theorem is referenced by: dfpred3g 5991 predbrg 6000 preddowncl 6007 wfisg 6015 wfr3g 7749 wfrlem1 7750 wfrdmcl 7760 wfrlem14 7765 wfrlem15 7766 wfrlem17 7768 wfr2a 7769 trpredeq3 32522 trpredlem1 32527 trpredtr 32530 trpredmintr 32531 trpredrec 32538 frpoinsg 32542 frmin 32545 frinsg 32548 elwlim 32571 frr3g 32582 fpr3g 32583 frrlem1 32584 frrlem12 32595 frrlem13 32596 fpr2 32601 frr2 32606 csbwrecsg 33985 |
Copyright terms: Public domain | W3C validator |