Theorem predeq3 6256

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

Syntax hints:   → wi 4   = wceq 1547  Predcpred 6251

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-xp 5624  df-cnv 5626  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252

This theorem is referenced by:  dfpred3g  6264  preddowncl  6283  frpoinsg  6294  frpoins3xpg  8080  frpoins3xp3g  8081  xpord2pred  8085  sexp2  8086  xpord3pred  8092  sexp3  8093  csbfrecsg  8224  fpr3g  8225  frrlem1  8226  frrlem12  8237  frrlem13  8238  fpr2a  8242  frrdmcl  8248  fprresex  8250  wfr3g  8259  ttrclselem1  9637  ttrclselem2  9638  frmin  9664  frinsg  9666  frr3g  9671  frr2  9675  elwlim  36049