Theorem predeq3 6304

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 2732	. 2 ⊢ 𝑅 = 𝑅
2		eqid 2732	. 2 ⊢ 𝐴 = 𝐴
3		predeq123 6301	. 2 ⊢ ((𝑅 = 𝑅 ∧ 𝐴 = 𝐴 ∧ 𝑋 = 𝑌) → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌))
4	1, 2, 3	mp3an12 1451	1 ⊢ (𝑋 = 𝑌 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌))

Syntax hints:   → wi 4   = wceq 1541  Predcpred 6299

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 2703

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 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-xp 5682  df-cnv 5684  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300

This theorem is referenced by:  dfpred3g  6312  predbrg  6322  preddowncl  6333  frpoinsg  6344  wfisgOLD  6355  frpoins3xpg  8125  frpoins3xp3g  8126  xpord2pred  8130  sexp2  8131  xpord3pred  8137  sexp3  8138  csbfrecsg  8268  fpr3g  8269  frrlem1  8270  frrlem12  8281  frrlem13  8282  fpr2a  8286  frrdmcl  8292  fprresex  8294  wfr3g  8306  wfrlem1OLD  8307  wfrdmclOLD  8316  wfrlem14OLD  8321  wfrlem15OLD  8322  wfrlem17OLD  8324  wfr2aOLD  8325  ttrclselem1  9719  ttrclselem2  9720  frmin  9743  frinsg  9745  frr3g  9750  frr2  9754  elwlim  34790