|   | 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 6322 | . 2 ⊢ ((𝑅 = 𝑅 ∧ 𝐴 = 𝐴 ∧ 𝑋 = 𝑌) → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌)) | |
| 4 | 1, 2, 3 | mp3an12 1453 | 1 ⊢ (𝑋 = 𝑌 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 = wceq 1540 Predcpred 6320 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-br 5144 df-opab 5206 df-xp 5691 df-cnv 5693 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 | 
| This theorem is referenced by: dfpred3g 6333 preddowncl 6353 frpoinsg 6364 wfisgOLD 6375 frpoins3xpg 8165 frpoins3xp3g 8166 xpord2pred 8170 sexp2 8171 xpord3pred 8177 sexp3 8178 csbfrecsg 8309 fpr3g 8310 frrlem1 8311 frrlem12 8322 frrlem13 8323 fpr2a 8327 frrdmcl 8333 fprresex 8335 wfr3g 8347 wfrlem1OLD 8348 wfrdmclOLD 8357 wfrlem14OLD 8362 wfrlem15OLD 8363 wfrlem17OLD 8365 wfr2aOLD 8366 ttrclselem1 9765 ttrclselem2 9766 frmin 9789 frinsg 9791 frr3g 9796 frr2 9800 elwlim 35824 | 
| Copyright terms: Public domain | W3C validator |