Theorem rneqi 5175

Description: Equality inference for range. (Contributed by NM, 4-Mar-2004.)

Hypothesis

Ref	Expression
rneqi.1	|- A = B

Assertion

Ref	Expression
rneqi	|- ran A = ran B

Proof of Theorem rneqi

Step	Hyp	Ref	Expression
1		rneqi.1	. 2 |- A = B
2		rneq 5174	. 2 |- ( A = B -> ran A = ran B )
3	1, 2	ax-mp 5	1 |- ran A = ran B

Syntax hints:   = wceq 1370   ran crn 4950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2808  df-v 3080  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3747  df-if 3901  df-sn 3987  df-pr 3989  df-op 3993  df-br 4402  df-opab 4460  df-cnv 4957  df-dm 4959  df-rn 4960

This theorem is referenced by:  rnmpt  5194  resima  5251  resima2  5252  ima0  5293  rnuni  5357  imaundi  5358  imaundir  5359  inimass  5362  dminxp  5387  imainrect  5388  xpima  5389  rnresv  5406  imacnvcnv  5412  rnpropg  5428  imadmres  5439  mptpreima  5440  dmco  5455  resdif  5770  fpr  6000  fliftfuns  6117  rnoprab  6284  rnmpt2  6311  elrnmpt2res  6315  curry1  6775  curry2  6778  fparlem3  6785  fparlem4  6786  qliftfuns  7298  xpassen  7516  sbthlem6  7537  dfsup3OLD  7806  hartogslem1  7868  rankwflemb  8112  fin23lem34  8627  axcc2lem  8717  axdc2lem  8729  fpwwe2lem13  8921  seqval  11935  0rest  14488  imasdsval2  14574  fulloppc  14952  oppchofcl  15190  oyoncl  15200  gsumwspan  15644  pmtrprfvalrn  16114  psgnsn  16146  psgnprfval2  16149  oppglsm  16263  efgredlemg  16361  efgredlemd  16363  dprdvalOLD  16610  pf1rcl  17909  mpfpf1  17911  pf1ind  17915  pjdm  18258  leordtvallem1  18947  leordtvallem2  18948  leordtval  18950  cnconst2  19020  ptcmplem1  19757  tgpconcomp  19816  fmucndlem  19999  fmucnd  20000  ucnextcn  20012  metusttoOLD  20265  metustto  20266  metustexhalfOLD  20271  metustexhalf  20272  metuustOLD  20279  metuust  20280  cfilucfil2OLD  20281  cfilucfil2  20282  metuelOLD  20285  metuel  20286  metutopOLD  20290  psmetutop  20291  restmetu  20295  metucnOLD  20296  metucn  20297  minveclem5  21053  minvec  21056  ovolgelb  21096  ovoliunlem1  21118  itg1addlem4  21311  itg2seq  21354  itg2i1fseq  21367  itg2cnlem1  21373  efifo  22137  logrn  22144  dfrelog  22151  dvrelog  22216  xrlimcnp  22496  usgrares1  23476  cusgrares  23533  ex-rn  23800  rngoueqz  24070  zerdivemp1  24074  rngoridfz  24075  bafval  24135  cnnvba  24222  minveco  24438  abrexexd  26043  imadifxp  26091  prsrn  26491  raddcn  26505  pl1cn  26531  sitgclbn  26874  ghomsn  27452  dfon4  28069  ellines  28328  ptrest  28574  ovoliunnfl  28582  voliunnfl  28584  rngonegmn1l  28904  rngonegmn1r  28905  rngoneglmul  28906  rngonegrmul  28907  zerdivemp1x  28910  isdrngo2  28913  rngokerinj  28930  iscrngo2  28947  idlnegcl  28971  1idl  28975  0rngo  28976  smprngopr  29001  prnc  29016  isfldidl  29017  isdmn3  29023  mzpmfp  29232  mzpmfpOLD  29233  usgra2adedglem1  30457