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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  Predcpred 6302

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-cnv 5659  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303

This theorem is used by:  dfpred3g  6315  preddowncl  6334  frpoinsg  6345  frpoins3xpg  8150  frpoins3xp3g  8151  xpord2pred  8155  sexp2  8156  xpord3pred  8162  sexp3  8163  csbfrecsg  8295  fpr3g  8296  frrlem1  8297  frrlem12  8308  frrlem13  8309  fpr2a  8313  frrdmcl  8319  fprresex  8321  wfr3g  8330  ttrclselem1  9719  ttrclselem2  9720  frmin  9746  frinsg  9748  frr3g  9753  frr2  9757  elwlim  36565