Theorem rneqi 5771

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

Hypothesis

Ref	Expression
rneqi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
rneqi	⊢ ran 𝐴 = ran 𝐵

Proof of Theorem rneqi

Step	Hyp	Ref	Expression
1		rneqi.1	. 2 ⊢ 𝐴 = 𝐵
2		rneq 5770	. 2 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
3	1, 2	ax-mp 5	1 ⊢ ran 𝐴 = ran 𝐵

Syntax hints:   = wceq 1538  ran crn 5520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-cnv 5527  df-dm 5529  df-rn 5530

This theorem is referenced by:  rnmpt  5791  resima  5852  resima2  5853  mptima  5908  ima0  5912  rnuni  5974  imaundi  5975  imaundir  5976  inimass  5979  dminxp  6004  imainrect  6005  xpima  6006  rnresv  6025  imacnvcnv  6030  rnpropg  6046  imadmres  6058  mptpreima  6059  dmco  6074  resdif  6610  fpr  6893  rnmptc  6946  fliftfuns  7046  rnoprab  7236  rnmpo  7263  elrnmpores  7267  curry1  7782  curry2  7785  fparlem3  7792  fparlem4  7793  fsplitfpar  7797  qliftfuns  8367  xpassen  8594  sbthlem6  8616  hartogslem1  8990  rankwflemb  9206  fin23lem34  9757  axcc2lem  9847  axdc2lem  9859  fpwwe2lem13  10053  seqval  13375  0rest  16695  imasdsval2  16781  fulloppc  17184  oppchofcl  17502  oyoncl  17512  gsumwspan  18003  pmtrprfvalrn  18608  psgnsn  18640  psgnprfval2  18643  oppglsm  18759  efgredlemg  18860  efgredlemd  18862  fincygsubgodd  19227  pjdm  20396  pf1rcl  20973  mpfpf1  20975  pf1ind  20979  leordtvallem1  21815  leordtvallem2  21816  leordtval  21818  cnconst2  21888  ptcmplem1  22657  tgpconncomp  22718  fmucndlem  22897  fmucnd  22898  ucnextcn  22910  metustto  23160  metustexhalf  23163  metuust  23167  cfilucfil2  23168  metuel  23171  psmetutop  23174  restmetu  23177  metucn  23178  minveclem5  24037  minvec  24040  ovolgelb  24084  ovoliunlem1  24106  itg1addlem4  24303  itg2seq  24346  itg2i1fseq  24359  itg2cnlem1  24365  efifo  25139  logrn  25150  dfrelog  25157  dvrelog  25228  xrlimcnp  25554  iedgedg  26843  edgiedgb  26847  edg0iedg0  26848  uhgrvtxedgiedgb  26929  uspgrf1oedg  26966  usgrf1oedg  26997  usgredg3  27006  ushgredgedg  27019  ushgredgedgloop  27021  usgrexmpledg  27052  0grsubgr  27068  uhgrspan1  27093  usgredgffibi  27114  dfnbgr3  27128  nbupgrres  27154  usgrnbcnvfv  27155  edginwlk  27424  wlkiswwlks2lem4  27658  wlkiswwlks2lem5  27659  clwlkclwwlk  27787  ex-rn  28225  bafval  28387  cnnvba  28462  minveco  28667  abrexexd  30277  imadifxp  30364  lsmsnorb  30999  prsrn  31268  raddcn  31282  pl1cn  31308  esumrnmpt2  31437  sitgclbn  31711  lfuhgr  32477  mvtval  32860  elmsubrn  32888  dfon4  33467  ellines  33726  rnmptsn  34752  f1omptsnlem  34753  icoreresf  34769  ptrest  35056  ovoliunnfl  35099  voliunnfl  35101  rngoueqz  35378  rngonegmn1l  35379  rngonegmn1r  35380  rngoneglmul  35381  rngonegrmul  35382  zerdivemp1x  35385  isdrngo2  35396  rngokerinj  35413  iscrngo2  35435  idlnegcl  35460  1idl  35464  0rngo  35465  smprngopr  35490  prnc  35505  isfldidl  35506  isdmn3  35512  rncnvepres  35721  imaopab  39413  mzpmfp  39688  dmnonrel  40290  imanonrel  40293  cnvrcl0  40325  ntrrn  40825  rnresun  41804  disjinfi  41820  rnmpt0  41849  imassmpt  41902  supxrleubrnmptf  42090  elicores  42170  limsupvaluz  42350  limsupmnflem  42362  limsupvaluz2  42380  limsup10ex  42415  liminf10ex  42416  liminflelimsuplem  42417  ioodvbdlimc1lem1  42573  ioodvbdlimc1  42575  ioodvbdlimc2  42577  fourierdlem42  42791  ioorrnopn  42947  subsaliuncl  42998  sge0sn  43018  sge0split  43048  sge0fodjrnlem  43055  sge0xaddlem2  43073  volicorescl  43192  hoidmvlelem3  43236  vonioolem2  43320  smflimsuplem1  43451  smflimsuplem3  43453  smflimsup  43459