Theorem rneqi 5931

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

This proof depends on syntax axioms:   = wceq 1570  ran crn 5659

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-cnv 5666  df-dm 5668  df-rn 5669

This theorem is used by:  rnmpt  5951  resima  6074  resima2  6075  mptima  6088  ima0  6093  rnuni  6158  imaundi  6159  imaundir  6160  inimass  6163  dminxp  6190  imainrect  6191  xpima  6192  rnresv  6214  imadifssranOLD  6221  imacnvcnv  6226  rnpropg  6242  imadmres  6254  mptpreima  6258  rnmpt0f  6263  dmco  6275  resdif  6876  fpr  7190  rnmptc  7244  fliftfuns  7353  rnoprab  7556  rnmpo  7585  elrnmpores  7590  curry1  8152  curry2  8155  fparlem3  8162  fparlem4  8163  fsplitfpar  8166  qliftfuns  8863  xpassen  9128  sbthlem6  9149  pwfir  9346  hartogslem1  9573  rnttrcl  9760  rankwflembOLD  9838  fin23lem34  10463  axcc2lem  10553  axdc2lem  10565  fpwwe2lem12  10766  seqval  14195  0rest  17650  imasdsval2  17738  fulloppc  18149  oppchofcl  18484  oyoncl  18494  gsumwspan  19092  pmtrprfvalrn  19753  psgnsn  19785  psgnprfval2  19788  oppglsm  19907  efgredlemg  20007  efgredlemd  20009  fincygsubgodd  20379  pjdm  22068  pf1rcl  22722  mpfpf1  22724  pf1ind  22728  leordtvallem1  23583  leordtvallem2  23584  leordtval  23586  cnconst2  23656  ptcmplem1  24426  tgpconncomp  24487  fmucndlem  24664  fmucnd  24665  ucnextcn  24677  metustto  24927  metustexhalf  24930  metuust  24934  cfilucfil2  24935  metuel  24938  psmetutop  24941  restmetu  24944  metucn  24945  minveclem5  25809  minvec  25812  ovolgelb  25856  ovoliunlem1  25878  itg1addlem4  26075  itg2seq  26118  itg2i1fseq  26131  itg2cnlem1  26137  efifo  26932  logrn  26943  dfrelog  26950  dvrelog  27022  xrlimcnp  27353  iedgedg  29685  edgiedgb  29689  edg0iedg0  29690  uhgrvtxedgiedgb  29771  lfuhgr  29783  uspgrf1oedg  29811  usgrf1oedg  29845  usgredg3  29854  ushgredgedg  29867  ushgredgedgloop  29869  usgrexmpledg  29900  0grsubgr  29916  uhgrspan1  29941  usgredgffibi  29962  dfnbgr3  29976  nbupgrres  30002  usgrnbcnvfv  30003  edginwlk  30272  wlkiswwlks2lem4  30518  wlkiswwlks2lem5  30519  clwlkclwwlk  30650  ex-rn  31098  bafval  31263  cnnvba  31338  minveco  31543  abrexexd  33204  imadifxp  33293  elrgspn  33906  elrgspnsubrun  33909  lsmsnorb  34050  prsrn  34658  raddcn  34672  pl1cn  34698  esumrnmpt2  34811  sitgclbn  35086  mvtval  36473  elmsubrn  36501  dfon4  36870  ellines  37132  rnmptsn  38526  f1omptsnlem  38527  icoreresf  38543  ptrest  38805  ovoliunnfl  38848  voliunnfl  38850  rngoueqz  39140  rngonegmn1l  39141  rngonegmn1r  39142  rngoneglmul  39143  rngonegrmul  39144  zerdivemp1x  39147  isdrngo2  39158  rngokerinj  39175  iscrngo2  39197  idlnegcl  39222  1idl  39226  0rngo  39227  smprngopr  39252  prnc  39267  isfldidl  39268  isdmn3  39274  rncnvepres  39507  rnqmap  39652  dfsuccl2  39668  imaopab  43552  mzpmfp  44024  dmnonrel  44851  imanonrel  44854  cnvrcl0  44886  ntrrn  45383  modelaxreplem2  46233  modelaxreplem3  46234  grpcanonhfstruct  46299  rnresun  46468  disjinfi  46480  imassmpt  46547  supxrleubrnmptf  46734  elicores  46818  limsupvaluz  46991  limsupmnflem  47003  limsupvaluz2  47021  limsup10ex  47056  liminf10ex  47057  liminflelimsuplem  47058  ioodvbdlimc1lem1  47214  ioodvbdlimc1  47216  ioodvbdlimc2  47218  fourierdlem42  47432  ioorrnopn  47588  subsaliuncl  47641  sge0sn  47662  sge0split  47692  sge0fodjrnlem  47699  sge0xaddlem2  47717  volicorescl  47836  hoidmvlelem3  47880  vonioolem2  47964  smflimsuplem1  48103  smflimsuplem3  48105  smflimsup  48111  fcoreslem2  48407  dfclnbgr3  49197  isuspgrim0lem  49264  upgrimtrlslem2  49276  usgrexmpl1edg  49395  usgrexmpl2edg  49400