Theorem rneqi 5894

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

Syntax hints:   = wceq 1542  ran crn 5633

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-cnv 5640  df-dm 5642  df-rn 5643

This theorem is referenced by:  rnmpt  5914  resima  5982  resima2  5983  mptima  6039  ima0  6044  rnuni  6114  imaundi  6115  imaundir  6116  inimass  6121  dminxp  6146  imainrect  6147  xpima  6148  rnresv  6167  imacnvcnv  6172  rnpropg  6188  imadmres  6200  mptpreima  6204  rnmpt0f  6209  dmco  6221  resdif  6803  fpr  7109  rnmptc  7163  fliftfuns  7270  rnoprab  7473  rnmpo  7501  elrnmpores  7506  curry1  8056  curry2  8059  fparlem3  8066  fparlem4  8067  fsplitfpar  8070  qliftfuns  8753  xpassen  9011  sbthlem6  9032  pwfir  9229  hartogslem1  9459  rnttrcl  9643  rankwflemb  9717  fin23lem34  10268  axcc2lem  10358  axdc2lem  10370  fpwwe2lem12  10565  seqval  13947  0rest  17361  imasdsval2  17449  fulloppc  17860  oppchofcl  18195  oyoncl  18205  gsumwspan  18783  pmtrprfvalrn  19429  psgnsn  19461  psgnprfval2  19464  oppglsm  19583  efgredlemg  19683  efgredlemd  19685  fincygsubgodd  20055  pjdm  21674  pf1rcl  22305  mpfpf1  22307  pf1ind  22311  leordtvallem1  23166  leordtvallem2  23167  leordtval  23169  cnconst2  23239  ptcmplem1  24008  tgpconncomp  24069  fmucndlem  24246  fmucnd  24247  ucnextcn  24259  metustto  24509  metustexhalf  24512  metuust  24516  cfilucfil2  24517  metuel  24520  psmetutop  24523  restmetu  24526  metucn  24527  minveclem5  25401  minvec  25404  ovolgelb  25449  ovoliunlem1  25471  itg1addlem4  25668  itg2seq  25711  itg2i1fseq  25724  itg2cnlem1  25730  efifo  26524  logrn  26535  dfrelog  26542  dvrelog  26614  xrlimcnp  26946  iedgedg  29135  edgiedgb  29139  edg0iedg0  29140  uhgrvtxedgiedgb  29221  uspgrf1oedg  29258  usgrf1oedg  29292  usgredg3  29301  ushgredgedg  29314  ushgredgedgloop  29316  usgrexmpledg  29347  0grsubgr  29363  uhgrspan1  29388  usgredgffibi  29409  dfnbgr3  29423  nbupgrres  29449  usgrnbcnvfv  29450  edginwlk  29720  wlkiswwlks2lem4  29957  wlkiswwlks2lem5  29958  clwlkclwwlk  30089  ex-rn  30527  bafval  30692  cnnvba  30767  minveco  30972  abrexexd  32596  imadifxp  32688  elrgspn  33340  elrgspnsubrun  33343  lsmsnorb  33484  prsrn  34093  raddcn  34107  pl1cn  34133  esumrnmpt2  34246  sitgclbn  34521  lfuhgr  35334  mvtval  35716  elmsubrn  35744  dfon4  36107  ellines  36368  rnmptsn  37590  f1omptsnlem  37591  icoreresf  37607  ptrest  37870  ovoliunnfl  37913  voliunnfl  37915  rngoueqz  38191  rngonegmn1l  38192  rngonegmn1r  38193  rngoneglmul  38194  rngonegrmul  38195  zerdivemp1x  38198  isdrngo2  38209  rngokerinj  38226  iscrngo2  38248  idlnegcl  38273  1idl  38277  0rngo  38278  smprngopr  38303  prnc  38318  isfldidl  38319  isdmn3  38325  rncnvepres  38560  rnqmap  38705  dfsuccl2  38721  imaopab  42603  mzpmfp  43104  dmnonrel  43946  imanonrel  43949  cnvrcl0  43981  ntrrn  44478  modelaxreplem2  45335  modelaxreplem3  45336  rnresun  45539  disjinfi  45551  imassmpt  45620  supxrleubrnmptf  45809  elicores  45893  limsupvaluz  46066  limsupmnflem  46078  limsupvaluz2  46096  limsup10ex  46131  liminf10ex  46132  liminflelimsuplem  46133  ioodvbdlimc1lem1  46289  ioodvbdlimc1  46291  ioodvbdlimc2  46293  fourierdlem42  46507  ioorrnopn  46663  subsaliuncl  46716  sge0sn  46737  sge0split  46767  sge0fodjrnlem  46774  sge0xaddlem2  46792  volicorescl  46911  hoidmvlelem3  46955  vonioolem2  47039  smflimsuplem1  47178  smflimsuplem3  47180  smflimsup  47186  fcoreslem2  47424  dfclnbgr3  48186  isuspgrim0lem  48253  upgrimtrlslem2  48265  usgrexmpl1edg  48384  usgrexmpl2edg  48389