Theorem rneqi 5273

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

Syntax hints:   = wceq 1475  ran crn 5039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-cnv 5046  df-dm 5048  df-rn 5049

This theorem is referenced by:  rnmpt  5292  resima  5351  resima2  5352  resima2OLD  5353  ima0  5400  rnuni  5463  imaundi  5464  imaundir  5465  inimass  5468  dminxp  5493  imainrect  5494  xpima  5495  rnresv  5512  imacnvcnv  5517  rnpropg  5533  imadmres  5544  mptpreima  5545  dmco  5560  resdif  6070  fpr  6326  fliftfuns  6464  rnoprab  6641  rnmpt2  6668  elrnmpt2res  6672  curry1  7156  curry2  7159  fparlem3  7166  fparlem4  7167  qliftfuns  7721  xpassen  7939  sbthlem6  7960  hartogslem1  8330  rankwflemb  8539  fin23lem34  9051  axcc2lem  9141  axdc2lem  9153  fpwwe2lem13  9343  seqval  12674  0rest  15913  imasdsval2  15999  fulloppc  16405  oppchofcl  16723  oyoncl  16733  gsumwspan  17206  pmtrprfvalrn  17731  psgnsn  17763  psgnprfval2  17766  oppglsm  17880  efgredlemg  17978  efgredlemd  17980  pf1rcl  19534  mpfpf1  19536  pf1ind  19540  pjdm  19870  leordtvallem1  20824  leordtvallem2  20825  leordtval  20827  cnconst2  20897  ptcmplem1  21666  tgpconcomp  21726  fmucndlem  21905  fmucnd  21906  ucnextcn  21918  metustto  22168  metustexhalf  22171  metuust  22175  cfilucfil2  22176  metuel  22179  psmetutop  22182  restmetu  22185  metucn  22186  minveclem5  23012  minvec  23015  ovolgelb  23055  ovoliunlem1  23077  itg1addlem4  23272  itg2seq  23315  itg2i1fseq  23328  itg2cnlem1  23334  efifo  24097  logrn  24109  dfrelog  24116  dvrelog  24183  xrlimcnp  24495  uhgrvtxedgiedgb  25810  usgrares1  25939  cusgrares  26001  ex-rn  26689  bafval  26843  cnnvba  26918  minveco  27124  abrexexd  28731  imadifxp  28796  prsrn  29289  raddcn  29303  pl1cn  29329  esumrnmpt2  29457  sitgclbn  29732  mvtval  30651  elmsubrn  30679  dfon4  31170  ellines  31429  rnmptsn  32358  f1omptsnlem  32359  icoreresf  32376  ptrest  32578  ovoliunnfl  32621  voliunnfl  32623  rngoueqz  32909  rngonegmn1l  32910  rngonegmn1r  32911  rngoneglmul  32912  rngonegrmul  32913  zerdivemp1x  32916  isdrngo2  32927  rngokerinj  32944  iscrngo2  32966  idlnegcl  32991  1idl  32995  0rngo  32996  smprngopr  33021  prnc  33036  isfldidl  33037  isdmn3  33043  mzpmfp  36328  dmnonrel  36915  imanonrel  36918  cnvrcl0  36951  ntrrn  37440  rnresun  38357  disjinfi  38375  rnmpt0  38407  elicores  38607  ioodvbdlimc1lem1  38821  ioodvbdlimc1  38823  ioodvbdlimc2  38825  fourierdlem42  39042  ioorrnopn  39201  subsaliuncl  39252  sge0sn  39272  sge0split  39302  sge0fodjrnlem  39309  sge0xaddlem2  39327  volicorescl  39443  hoidmvlelem3  39487  vonioolem2  39572  uspgrf1oedg  40403  usgrf1oedg  40434  usgredg3  40443  ushgredgedga  40456  ushgredgedgaloop  40458  usgrexmpledg  40486  0grsubgr  40502  uhgrspan1  40527  usgredgffibi  40543  dfnbgr3  40562  nbupgrres  40592  usgrnbcnvfv  40593  edginwlk  40839  1wlkiswwlks2lem4  41069  1wlkiswwlks2lem5  41070  clwlkclwwlk  41211