Theorem rneqi 5886

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 5885	. 2 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
3	1, 2	ax-mp 5	1 ⊢ ran 𝐴 = ran 𝐵

Syntax hints:   = wceq 1541  ran crn 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-cnv 5632  df-dm 5634  df-rn 5635

This theorem is referenced by:  rnmpt  5906  resima  5974  resima2  5975  mptima  6031  ima0  6036  rnuni  6106  imaundi  6107  imaundir  6108  inimass  6113  dminxp  6138  imainrect  6139  xpima  6140  rnresv  6159  imacnvcnv  6164  rnpropg  6180  imadmres  6192  mptpreima  6196  rnmpt0f  6201  dmco  6213  resdif  6795  fpr  7099  rnmptc  7153  fliftfuns  7260  rnoprab  7463  rnmpo  7491  elrnmpores  7496  curry1  8046  curry2  8049  fparlem3  8056  fparlem4  8057  fsplitfpar  8060  qliftfuns  8741  xpassen  8999  sbthlem6  9020  pwfir  9217  hartogslem1  9447  rnttrcl  9631  rankwflemb  9705  fin23lem34  10256  axcc2lem  10346  axdc2lem  10358  fpwwe2lem12  10553  seqval  13935  0rest  17349  imasdsval2  17437  fulloppc  17848  oppchofcl  18183  oyoncl  18193  gsumwspan  18771  pmtrprfvalrn  19417  psgnsn  19449  psgnprfval2  19452  oppglsm  19571  efgredlemg  19671  efgredlemd  19673  fincygsubgodd  20043  pjdm  21662  pf1rcl  22293  mpfpf1  22295  pf1ind  22299  leordtvallem1  23154  leordtvallem2  23155  leordtval  23157  cnconst2  23227  ptcmplem1  23996  tgpconncomp  24057  fmucndlem  24234  fmucnd  24235  ucnextcn  24247  metustto  24497  metustexhalf  24500  metuust  24504  cfilucfil2  24505  metuel  24508  psmetutop  24511  restmetu  24514  metucn  24515  minveclem5  25389  minvec  25392  ovolgelb  25437  ovoliunlem1  25459  itg1addlem4  25656  itg2seq  25699  itg2i1fseq  25712  itg2cnlem1  25718  efifo  26512  logrn  26523  dfrelog  26530  dvrelog  26602  xrlimcnp  26934  iedgedg  29123  edgiedgb  29127  edg0iedg0  29128  uhgrvtxedgiedgb  29209  uspgrf1oedg  29246  usgrf1oedg  29280  usgredg3  29289  ushgredgedg  29302  ushgredgedgloop  29304  usgrexmpledg  29335  0grsubgr  29351  uhgrspan1  29376  usgredgffibi  29397  dfnbgr3  29411  nbupgrres  29437  usgrnbcnvfv  29438  edginwlk  29708  wlkiswwlks2lem4  29945  wlkiswwlks2lem5  29946  clwlkclwwlk  30077  ex-rn  30515  bafval  30679  cnnvba  30754  minveco  30959  abrexexd  32584  imadifxp  32676  elrgspn  33328  elrgspnsubrun  33331  lsmsnorb  33472  prsrn  34072  raddcn  34086  pl1cn  34112  esumrnmpt2  34225  sitgclbn  34500  lfuhgr  35312  mvtval  35694  elmsubrn  35722  dfon4  36085  ellines  36346  rnmptsn  37540  f1omptsnlem  37541  icoreresf  37557  ptrest  37820  ovoliunnfl  37863  voliunnfl  37865  rngoueqz  38141  rngonegmn1l  38142  rngonegmn1r  38143  rngoneglmul  38144  rngonegrmul  38145  zerdivemp1x  38148  isdrngo2  38159  rngokerinj  38176  iscrngo2  38198  idlnegcl  38223  1idl  38227  0rngo  38228  smprngopr  38253  prnc  38268  isfldidl  38269  isdmn3  38275  rncnvepres  38502  dfsuccl2  38644  imaopab  42487  mzpmfp  42989  dmnonrel  43831  imanonrel  43834  cnvrcl0  43866  ntrrn  44363  modelaxreplem2  45220  modelaxreplem3  45221  rnresun  45424  disjinfi  45436  imassmpt  45506  supxrleubrnmptf  45695  elicores  45779  limsupvaluz  45952  limsupmnflem  45964  limsupvaluz2  45982  limsup10ex  46017  liminf10ex  46018  liminflelimsuplem  46019  ioodvbdlimc1lem1  46175  ioodvbdlimc1  46177  ioodvbdlimc2  46179  fourierdlem42  46393  ioorrnopn  46549  subsaliuncl  46602  sge0sn  46623  sge0split  46653  sge0fodjrnlem  46660  sge0xaddlem2  46678  volicorescl  46797  hoidmvlelem3  46841  vonioolem2  46925  smflimsuplem1  47064  smflimsuplem3  47066  smflimsup  47072  fcoreslem2  47310  dfclnbgr3  48072  isuspgrim0lem  48139  upgrimtrlslem2  48151  usgrexmpl1edg  48270  usgrexmpl2edg  48275