Theorem rneqd 3357

Description: Equality deduction for range.

Hypothesis

Ref	Expression
rneqd.1	|- (ph -> A = B)

Assertion

Ref	Expression
rneqd	|- (ph -> ran A = ran B)

Proof of Theorem rneqd

Step	Hyp	Ref	Expression
1		rneqd.1	. 2 |- (ph -> A = B)
2		rneq 3355	. 2 |- (A = B -> ran A = ran B)
3	1, 2	syl 10	1 |- (ph -> ran A = ran B)

Syntax hints:   -> wi 3   = wceq 960  ran crn 3187

This theorem is referenced by:  imaeq1 3417  imaeq2 3418  resiima 3435  elxp4 3469  elxp5 3470  rnxpss 3490  funimacnv 3587  2ndval 4098  fo2nd 4108  f2ndres 4110  curry1 4114  en1 4444  xpassen 4460  xpdom2 4461  sbthlem4 4469  fodomr 4502  xpmapenlem2 4517  xpmapenlem4 4519  xpmapenlem5 4520  mapunen 4522  xpnnen 7532  blrn 7867  opnfval 7883  grplactf1o 8123  subgrnss 8144  vcoprne 8223  bafval 8248  kbass5 10077  elpjrn 10142  pj3i 10161  cayleythlem 10438  aidm 10704

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-10 970  ax-11 971  ax-12 972  ax-13 973  ax-14 974  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1127  ax-10o 1144  ax-16 1214  ax-11o 1222  ax-ext 1464  ax-sep 2718  ax-pow 2758  ax-pr 2795

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 985  df-sb 1176  df-eu 1386  df-mo 1387  df-clab 1470  df-cleq 1475  df-clel 1478  df-ne 1594  df-v 1819  df-dif 2060  df-un 2061  df-in 2062  df-ss 2064  df-nul 2292  df-pw 2414  df-sn 2424  df-pr 2425  df-op 2428  df-br 2635  df-opab 2682  df-cnv 3202  df-dm 3204  df-rn 3205

Copyright terms: Public domain