![]() |
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 2737 | . 2 ⊢ 𝑅 = 𝑅 | |
2 | eqid 2737 | . 2 ⊢ 𝐴 = 𝐴 | |
3 | predeq123 6252 | . 2 ⊢ ((𝑅 = 𝑅 ∧ 𝐴 = 𝐴 ∧ 𝑋 = 𝑌) → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌)) | |
4 | 1, 2, 3 | mp3an12 1451 | 1 ⊢ (𝑋 = 𝑌 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 Predcpred 6250 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2715 df-cleq 2729 df-clel 2815 df-rab 3406 df-v 3445 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-br 5104 df-opab 5166 df-xp 5637 df-cnv 5639 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6251 |
This theorem is referenced by: dfpred3g 6263 predbrg 6273 preddowncl 6284 frpoinsg 6295 wfisgOLD 6306 frpoins3xpg 8064 frpoins3xp3g 8065 xpord2pred 8069 sexp2 8070 xpord3pred 8076 sexp3 8077 csbfrecsg 8207 fpr3g 8208 frrlem1 8209 frrlem12 8220 frrlem13 8221 fpr2a 8225 frrdmcl 8231 fprresex 8233 wfr3g 8245 wfrlem1OLD 8246 wfrdmclOLD 8255 wfrlem14OLD 8260 wfrlem15OLD 8261 wfrlem17OLD 8263 wfr2aOLD 8264 ttrclselem1 9619 ttrclselem2 9620 frmin 9643 frinsg 9645 frr3g 9650 frr2 9654 elwlim 34214 |
Copyright terms: Public domain | W3C validator |