Theorem predeq3 6311

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  Predcpred 6306

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-xp 5657  df-cnv 5659  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6307

This theorem is used by:  dfpred3g  6319  preddowncl  6338  frpoinsg  6349  frpoins3xpg  8164  frpoins3xp3g  8165  xpord2pred  8169  sexp2  8170  xpord3pred  8176  sexp3  8177  csbfrecsg  8310  fpr3g  8311  frrlem1  8312  frrlem12  8323  frrlem13  8324  fpr2a  8328  frrdmcl  8334  fprresex  8336  wfr3g  8345  ttrclselem1  9733  ttrclselem2  9734  frmin  9760  frinsg  9762  frr3g  9767  frr2  9771  elwlim  36709