Theorem rneqi 5892

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

Syntax hints:   = wceq 1542  ran crn 5632

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  rnmpt  5912  resima  5980  resima2  5981  mptima  6037  ima0  6042  rnuni  6112  imaundi  6113  imaundir  6114  inimass  6119  dminxp  6144  imainrect  6145  xpima  6146  rnresv  6165  imacnvcnv  6170  rnpropg  6186  imadmres  6198  mptpreima  6202  rnmpt0f  6207  dmco  6219  resdif  6801  fpr  7108  rnmptc  7162  fliftfuns  7269  rnoprab  7472  rnmpo  7500  elrnmpores  7505  curry1  8054  curry2  8057  fparlem3  8064  fparlem4  8065  fsplitfpar  8068  qliftfuns  8751  xpassen  9009  sbthlem6  9030  pwfir  9227  hartogslem1  9457  rnttrcl  9643  rankwflemb  9717  fin23lem34  10268  axcc2lem  10358  axdc2lem  10370  fpwwe2lem12  10565  seqval  13974  0rest  17392  imasdsval2  17480  fulloppc  17891  oppchofcl  18226  oyoncl  18236  gsumwspan  18814  pmtrprfvalrn  19463  psgnsn  19495  psgnprfval2  19498  oppglsm  19617  efgredlemg  19717  efgredlemd  19719  fincygsubgodd  20089  pjdm  21687  pf1rcl  22314  mpfpf1  22316  pf1ind  22320  leordtvallem1  23175  leordtvallem2  23176  leordtval  23178  cnconst2  23248  ptcmplem1  24017  tgpconncomp  24078  fmucndlem  24255  fmucnd  24256  ucnextcn  24268  metustto  24518  metustexhalf  24521  metuust  24525  cfilucfil2  24526  metuel  24529  psmetutop  24532  restmetu  24535  metucn  24536  minveclem5  25400  minvec  25403  ovolgelb  25447  ovoliunlem1  25469  itg1addlem4  25666  itg2seq  25709  itg2i1fseq  25722  itg2cnlem1  25728  efifo  26511  logrn  26522  dfrelog  26529  dvrelog  26601  xrlimcnp  26932  iedgedg  29119  edgiedgb  29123  edg0iedg0  29124  uhgrvtxedgiedgb  29205  uspgrf1oedg  29242  usgrf1oedg  29276  usgredg3  29285  ushgredgedg  29298  ushgredgedgloop  29300  usgrexmpledg  29331  0grsubgr  29347  uhgrspan1  29372  usgredgffibi  29393  dfnbgr3  29407  nbupgrres  29433  usgrnbcnvfv  29434  edginwlk  29703  wlkiswwlks2lem4  29940  wlkiswwlks2lem5  29941  clwlkclwwlk  30072  ex-rn  30510  bafval  30675  cnnvba  30750  minveco  30955  abrexexd  32579  imadifxp  32671  elrgspn  33307  elrgspnsubrun  33310  lsmsnorb  33451  prsrn  34059  raddcn  34073  pl1cn  34099  esumrnmpt2  34212  sitgclbn  34487  lfuhgr  35300  mvtval  35682  elmsubrn  35710  dfon4  36073  ellines  36334  rnmptsn  37651  f1omptsnlem  37652  icoreresf  37668  ptrest  37940  ovoliunnfl  37983  voliunnfl  37985  rngoueqz  38261  rngonegmn1l  38262  rngonegmn1r  38263  rngoneglmul  38264  rngonegrmul  38265  zerdivemp1x  38268  isdrngo2  38279  rngokerinj  38296  iscrngo2  38318  idlnegcl  38343  1idl  38347  0rngo  38348  smprngopr  38373  prnc  38388  isfldidl  38389  isdmn3  38395  rncnvepres  38630  rnqmap  38775  dfsuccl2  38791  imaopab  42672  mzpmfp  43179  dmnonrel  44017  imanonrel  44020  cnvrcl0  44052  ntrrn  44549  modelaxreplem2  45406  modelaxreplem3  45407  rnresun  45610  disjinfi  45622  imassmpt  45691  supxrleubrnmptf  45879  elicores  45963  limsupvaluz  46136  limsupmnflem  46148  limsupvaluz2  46166  limsup10ex  46201  liminf10ex  46202  liminflelimsuplem  46203  ioodvbdlimc1lem1  46359  ioodvbdlimc1  46361  ioodvbdlimc2  46363  fourierdlem42  46577  ioorrnopn  46733  subsaliuncl  46786  sge0sn  46807  sge0split  46837  sge0fodjrnlem  46844  sge0xaddlem2  46862  volicorescl  46981  hoidmvlelem3  47025  vonioolem2  47109  smflimsuplem1  47248  smflimsuplem3  47250  smflimsup  47256  fcoreslem2  47512  dfclnbgr3  48302  isuspgrim0lem  48369  upgrimtrlslem2  48381  usgrexmpl1edg  48500  usgrexmpl2edg  48505