Theorem rneq 3355

Description: Equality theorem for range.

Assertion

Ref	Expression
rneq	|- (A = B -> ran A = ran B)

Proof of Theorem rneq

Step	Hyp	Ref	Expression
1		cnveq 3308	. . 3 |- (A = B -> `'A = `'B)
2	1	dmeqd 3329	. 2 |- (A = B -> dom `' A = dom `' B)
3		df-rn 3205	. 2 |- ran A = dom `' A
4		df-rn 3205	. 2 |- ran B = dom `' B
5	2, 3, 4	3eqtr4g 1538	1 |- (A = B -> ran A = ran B)

Syntax hints:   -> wi 3   = wceq 960  `'ccnv 3185  dom cdm 3186  ran crn 3187

This theorem is referenced by:  rneqi 3356  rneqd 3357  feq1 3636  foeq1 3684  fvres 3750  fconst5 3864  tz7.44-3 3946  rdglem2 3954  map0e 4360  aceq5lem3 4754  numthlem 4800  numth 4801  zorn2lem1 4805  zorn2 4813  infxpidmlem4 7588  infxpidmlem8 7592  infxpidmlem10 7594  infmap2lem2 7613  bcth 8058  grpidval 8083  grpinvfval 8091  grpdivfval 8106  isabl 8126  isring 8166  ringi 8167  vci 8192  isvclem 8221  isnvlem 8254  nvi 8258  isphg 8501  pj11i 9680  pjss1coi 10115  elghomlem1 10407  ghomgrplem 10414  elgiso 10423  vri 10522  isalg 10674  algi 10681

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