Theorem rneqi 5352

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 5351	. 2 |- ( A = B -> ran A = ran B )
3	1, 2	ax-mp 5	1 |- ran A = ran B

Syntax hints:   = wceq 1483   ran crn 5115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-cnv 5122  df-dm 5124  df-rn 5125

This theorem is referenced by:  rnmpt  5371  resima  5431  resima2  5432  resima2OLD  5433  ima0  5481  rnuni  5544  imaundi  5545  imaundir  5546  inimass  5549  dminxp  5574  imainrect  5575  xpima  5576  rnresv  5594  imacnvcnv  5599  rnpropg  5615  imadmres  5627  mptpreima  5628  dmco  5643  resdif  6157  fpr  6421  fliftfuns  6564  rnoprab  6743  rnmpt2  6770  elrnmpt2res  6774  curry1  7269  curry2  7272  fparlem3  7279  fparlem4  7280  qliftfuns  7834  xpassen  8054  sbthlem6  8075  hartogslem1  8447  rankwflemb  8656  fin23lem34  9168  axcc2lem  9258  axdc2lem  9270  fpwwe2lem13  9464  seqval  12812  0rest  16090  imasdsval2  16176  fulloppc  16582  oppchofcl  16900  oyoncl  16910  gsumwspan  17383  pmtrprfvalrn  17908  psgnsn  17940  psgnprfval2  17943  oppglsm  18057  efgredlemg  18155  efgredlemd  18157  pf1rcl  19713  mpfpf1  19715  pf1ind  19719  pjdm  20051  leordtvallem1  21014  leordtvallem2  21015  leordtval  21017  cnconst2  21087  ptcmplem1  21856  tgpconncomp  21916  fmucndlem  22095  fmucnd  22096  ucnextcn  22108  metustto  22358  metustexhalf  22361  metuust  22365  cfilucfil2  22366  metuel  22369  psmetutop  22372  restmetu  22375  metucn  22376  minveclem5  23204  minvec  23207  ovolgelb  23248  ovoliunlem1  23270  itg1addlem4  23466  itg2seq  23509  itg2i1fseq  23522  itg2cnlem1  23528  efifo  24293  logrn  24305  dfrelog  24312  dvrelog  24383  xrlimcnp  24695  iedgedg  25943  edgiedgb  25947  edg0iedg0  25949  uhgrvtxedgiedgb  26031  uspgrf1oedg  26068  usgrf1oedg  26099  usgredg3  26108  ushgredgedg  26121  ushgredgedgloop  26123  usgrexmpledg  26154  0grsubgr  26170  uhgrspan1  26195  usgredgffibi  26216  dfnbgr3  26236  nbupgrres  26266  usgrnbcnvfv  26267  edginwlk  26530  edginwlkOLD  26531  wlkiswwlks2lem4  26758  wlkiswwlks2lem5  26759  clwlkclwwlk  26903  ex-rn  27297  bafval  27459  cnnvba  27534  minveco  27740  abrexexd  29347  imadifxp  29414  prsrn  29961  raddcn  29975  pl1cn  30001  esumrnmpt2  30130  sitgclbn  30405  mvtval  31397  elmsubrn  31425  dfon4  32000  ellines  32259  rnmptsn  33182  f1omptsnlem  33183  icoreresf  33200  ptrest  33408  ovoliunnfl  33451  voliunnfl  33453  rngoueqz  33739  rngonegmn1l  33740  rngonegmn1r  33741  rngoneglmul  33742  rngonegrmul  33743  zerdivemp1x  33746  isdrngo2  33757  rngokerinj  33774  iscrngo2  33796  idlnegcl  33821  1idl  33825  0rngo  33826  smprngopr  33851  prnc  33866  isfldidl  33867  isdmn3  33873  rncnvepres  34073  mzpmfp  37310  dmnonrel  37896  imanonrel  37899  cnvrcl0  37932  ntrrn  38420  rnresun  39362  disjinfi  39380  rnmpt0  39412  mptima  39437  imassmpt  39481  supxrleubrnmptf  39680  elicores  39760  limsupvaluz  39940  limsupmnflem  39952  limsupvaluz2  39970  limsup10ex  40005  liminf10ex  40006  liminflelimsuplem  40007  ioodvbdlimc1lem1  40146  ioodvbdlimc1  40148  ioodvbdlimc2  40150  fourierdlem42  40366  ioorrnopn  40525  subsaliuncl  40576  sge0sn  40596  sge0split  40626  sge0fodjrnlem  40633  sge0xaddlem2  40651  volicorescl  40767  hoidmvlelem3  40811  vonioolem2  40895  smflimsuplem1  41026  smflimsuplem3  41028  smflimsup  41034