![]() |
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 2733 | . 2 ⊢ 𝑅 = 𝑅 | |
2 | eqid 2733 | . 2 ⊢ 𝐴 = 𝐴 | |
3 | predeq123 6255 | . 2 ⊢ ((𝑅 = 𝑅 ∧ 𝐴 = 𝐴 ∧ 𝑋 = 𝑌) → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌)) | |
4 | 1, 2, 3 | mp3an12 1452 | 1 ⊢ (𝑋 = 𝑌 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 Predcpred 6253 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3407 df-v 3446 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4284 df-if 4488 df-sn 4588 df-pr 4590 df-op 4594 df-br 5107 df-opab 5169 df-xp 5640 df-cnv 5642 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-pred 6254 |
This theorem is referenced by: dfpred3g 6266 predbrg 6276 preddowncl 6287 frpoinsg 6298 wfisgOLD 6309 frpoins3xpg 8073 frpoins3xp3g 8074 xpord2pred 8078 sexp2 8079 xpord3pred 8085 sexp3 8086 csbfrecsg 8216 fpr3g 8217 frrlem1 8218 frrlem12 8229 frrlem13 8230 fpr2a 8234 frrdmcl 8240 fprresex 8242 wfr3g 8254 wfrlem1OLD 8255 wfrdmclOLD 8264 wfrlem14OLD 8269 wfrlem15OLD 8270 wfrlem17OLD 8272 wfr2aOLD 8273 ttrclselem1 9666 ttrclselem2 9667 frmin 9690 frinsg 9692 frr3g 9697 frr2 9701 elwlim 34454 |
Copyright terms: Public domain | W3C validator |