![]() |
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 2726 | . 2 ⊢ 𝑅 = 𝑅 | |
2 | eqid 2726 | . 2 ⊢ 𝐴 = 𝐴 | |
3 | predeq123 6304 | . 2 ⊢ ((𝑅 = 𝑅 ∧ 𝐴 = 𝐴 ∧ 𝑋 = 𝑌) → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌)) | |
4 | 1, 2, 3 | mp3an12 1448 | 1 ⊢ (𝑋 = 𝑌 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1534 Predcpred 6302 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3421 df-v 3465 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4324 df-if 4525 df-sn 4625 df-pr 4627 df-op 4631 df-br 5145 df-opab 5207 df-xp 5679 df-cnv 5681 df-dm 5683 df-rn 5684 df-res 5685 df-ima 5686 df-pred 6303 |
This theorem is referenced by: dfpred3g 6315 preddowncl 6335 frpoinsg 6346 wfisgOLD 6357 frpoins3xpg 8144 frpoins3xp3g 8145 xpord2pred 8149 sexp2 8150 xpord3pred 8156 sexp3 8157 csbfrecsg 8289 fpr3g 8290 frrlem1 8291 frrlem12 8302 frrlem13 8303 fpr2a 8307 frrdmcl 8313 fprresex 8315 wfr3g 8327 wfrlem1OLD 8328 wfrdmclOLD 8337 wfrlem14OLD 8342 wfrlem15OLD 8343 wfrlem17OLD 8345 wfr2aOLD 8346 ttrclselem1 9759 ttrclselem2 9760 frmin 9783 frinsg 9785 frr3g 9790 frr2 9794 elwlim 35658 |
Copyright terms: Public domain | W3C validator |