Theorem predeq3 6266

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

Syntax hints:   → wi 4   = wceq 1540  Predcpred 6261

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-xp 5637  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262

This theorem is referenced by:  dfpred3g  6274  preddowncl  6293  frpoinsg  6304  frpoins3xpg  8096  frpoins3xp3g  8097  xpord2pred  8101  sexp2  8102  xpord3pred  8108  sexp3  8109  csbfrecsg  8240  fpr3g  8241  frrlem1  8242  frrlem12  8253  frrlem13  8254  fpr2a  8258  frrdmcl  8264  fprresex  8266  wfr3g  8275  ttrclselem1  9654  ttrclselem2  9655  frmin  9678  frinsg  9680  frr3g  9685  frr2  9689  elwlim  35784