Theorem predeq3 6307

Description: Equality theorem for the predecessor class. (Contributed by Scott Fenton, 2-Feb-2011.)

Assertion

Ref	Expression
predeq3	⊢ (𝑋 = 𝑌 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌))

Proof of Theorem predeq3

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(𝑅, 𝐴, 𝑌))

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