Theorem rneqi 5774

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

Syntax hints:   = wceq 1542  ran crn 5520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3399  df-un 3846  df-in 3848  df-ss 3858  df-sn 4514  df-pr 4516  df-op 4520  df-br 5028  df-opab 5090  df-cnv 5527  df-dm 5529  df-rn 5530

This theorem is referenced by:  rnmpt  5792  resima  5853  resima2  5854  mptima  5909  ima0  5913  rnuni  5975  imaundi  5976  imaundir  5977  inimass  5981  dminxp  6006  imainrect  6007  xpima  6008  rnresv  6027  imacnvcnv  6032  rnpropg  6048  imadmres  6060  mptpreima  6064  rnmpt0f  6069  dmco  6081  resdif  6632  fpr  6920  rnmptc  6973  fliftfuns  7074  rnoprab  7265  rnmpo  7293  elrnmpores  7297  curry1  7818  curry2  7821  fparlem3  7828  fparlem4  7829  fsplitfpar  7833  qliftfuns  8408  xpassen  8653  sbthlem6  8675  pwfir  8767  hartogslem1  9072  rankwflemb  9288  fin23lem34  9839  axcc2lem  9929  axdc2lem  9941  fpwwe2lem12  10135  seqval  13464  0rest  16799  imasdsval2  16885  fulloppc  17290  oppchofcl  17619  oyoncl  17629  gsumwspan  18120  pmtrprfvalrn  18727  psgnsn  18759  psgnprfval2  18762  oppglsm  18878  efgredlemg  18979  efgredlemd  18981  fincygsubgodd  19346  pjdm  20516  pf1rcl  21112  mpfpf1  21114  pf1ind  21118  leordtvallem1  21954  leordtvallem2  21955  leordtval  21957  cnconst2  22027  ptcmplem1  22796  tgpconncomp  22857  fmucndlem  23036  fmucnd  23037  ucnextcn  23049  metustto  23299  metustexhalf  23302  metuust  23306  cfilucfil2  23307  metuel  23310  psmetutop  23313  restmetu  23316  metucn  23317  minveclem5  24178  minvec  24181  ovolgelb  24225  ovoliunlem1  24247  itg1addlem4  24444  itg2seq  24487  itg2i1fseq  24500  itg2cnlem1  24506  efifo  25283  logrn  25294  dfrelog  25301  dvrelog  25372  xrlimcnp  25698  iedgedg  26987  edgiedgb  26991  edg0iedg0  26992  uhgrvtxedgiedgb  27073  uspgrf1oedg  27110  usgrf1oedg  27141  usgredg3  27150  ushgredgedg  27163  ushgredgedgloop  27165  usgrexmpledg  27196  0grsubgr  27212  uhgrspan1  27237  usgredgffibi  27258  dfnbgr3  27272  nbupgrres  27298  usgrnbcnvfv  27299  edginwlk  27568  wlkiswwlks2lem4  27802  wlkiswwlks2lem5  27803  clwlkclwwlk  27931  ex-rn  28369  bafval  28531  cnnvba  28606  minveco  28811  abrexexd  30420  imadifxp  30506  lsmsnorb  31143  prsrn  31429  raddcn  31443  pl1cn  31469  esumrnmpt2  31598  sitgclbn  31872  lfuhgr  32642  mvtval  33025  elmsubrn  33053  dfon4  33825  ellines  34084  rnmptsn  35118  f1omptsnlem  35119  icoreresf  35135  ptrest  35388  ovoliunnfl  35431  voliunnfl  35433  rngoueqz  35710  rngonegmn1l  35711  rngonegmn1r  35712  rngoneglmul  35713  rngonegrmul  35714  zerdivemp1x  35717  isdrngo2  35728  rngokerinj  35745  iscrngo2  35767  idlnegcl  35792  1idl  35796  0rngo  35797  smprngopr  35822  prnc  35837  isfldidl  35838  isdmn3  35844  rncnvepres  36051  imaopab  39773  mzpmfp  40125  dmnonrel  40727  imanonrel  40730  cnvrcl0  40762  ntrrn  41262  rnresun  42238  disjinfi  42253  imassmpt  42331  supxrleubrnmptf  42515  elicores  42595  limsupvaluz  42775  limsupmnflem  42787  limsupvaluz2  42805  limsup10ex  42840  liminf10ex  42841  liminflelimsuplem  42842  ioodvbdlimc1lem1  42998  ioodvbdlimc1  43000  ioodvbdlimc2  43002  fourierdlem42  43216  ioorrnopn  43372  subsaliuncl  43423  sge0sn  43443  sge0split  43473  sge0fodjrnlem  43480  sge0xaddlem2  43498  volicorescl  43617  hoidmvlelem3  43661  vonioolem2  43745  smflimsuplem1  43876  smflimsuplem3  43878  smflimsup  43884  fcoreslem2  44080