MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  predeq3 Structured version   Visualization version   GIF version

Theorem predeq3 6124
Description: Equality theorem for the predecessor class. (Contributed by Scott Fenton, 2-Feb-2011.)
Assertion
Ref Expression
predeq3 (𝑋 = 𝑌 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌))

Proof of Theorem predeq3
StepHypRef Expression
1 eqid 2801 . 2 𝑅 = 𝑅
2 eqid 2801 . 2 𝐴 = 𝐴
3 predeq123 6121 . 2 ((𝑅 = 𝑅𝐴 = 𝐴𝑋 = 𝑌) → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌))
41, 2, 3mp3an12 1448 1 (𝑋 = 𝑌 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  Predcpred 6119
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-rab 3118  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034  df-opab 5096  df-xp 5529  df-cnv 5531  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120
This theorem is referenced by:  dfpred3g  6131  predbrg  6140  preddowncl  6147  wfisg  6155  wfr3g  7940  wfrlem1  7941  wfrdmcl  7950  wfrlem14  7955  wfrlem15  7956  wfrlem17  7958  wfr2a  7959  trpredeq3  33169  trpredlem1  33174  trpredtr  33177  trpredmintr  33178  trpredrec  33185  frpoinsg  33189  frmin  33192  frinsg  33195  elwlim  33218  frr3g  33229  fpr3g  33230  frrlem1  33231  frrlem12  33242  frrlem13  33243  fpr2  33248  frr2  33253  csbwrecsg  34739
  Copyright terms: Public domain W3C validator