Theorem rneqi 5597

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

Syntax hints:   = wceq 1601  ran crn 5356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-rab 3098  df-v 3399  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-nul 4141  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-br 4887  df-opab 4949  df-cnv 5363  df-dm 5365  df-rn 5366

This theorem is referenced by:  rnmpt  5617  resima  5680  resima2  5681  ima0  5735  rnuni  5798  imaundi  5799  imaundir  5800  inimass  5803  dminxp  5828  imainrect  5829  xpima  5830  rnresv  5848  imacnvcnv  5853  rnpropg  5869  imadmres  5881  mptpreima  5882  dmco  5897  resdif  6411  fpr  6687  fliftfuns  6836  rnoprab  7020  rnmpt2  7047  elrnmpt2res  7051  curry1  7550  curry2  7553  fparlem3  7560  fparlem4  7561  qliftfuns  8117  xpassen  8342  sbthlem6  8363  hartogslem1  8736  rankwflemb  8953  fin23lem34  9503  axcc2lem  9593  axdc2lem  9605  fpwwe2lem13  9799  seqval  13130  0rest  16476  imasdsval2  16562  fulloppc  16967  oppchofcl  17286  oyoncl  17296  gsumwspan  17770  pmtrprfvalrn  18291  psgnsn  18324  psgnprfval2  18327  oppglsm  18441  efgredlemg  18540  efgredlemd  18542  pf1rcl  20109  mpfpf1  20111  pf1ind  20115  pjdm  20450  leordtvallem1  21422  leordtvallem2  21423  leordtval  21425  cnconst2  21495  ptcmplem1  22264  tgpconncomp  22324  fmucndlem  22503  fmucnd  22504  ucnextcn  22516  metustto  22766  metustexhalf  22769  metuust  22773  cfilucfil2  22774  metuel  22777  psmetutop  22780  restmetu  22783  metucn  22784  minveclem5  23639  minvec  23642  ovolgelb  23684  ovoliunlem1  23706  itg1addlem4  23903  itg2seq  23946  itg2i1fseq  23959  itg2cnlem1  23965  efifo  24731  logrn  24742  dfrelog  24749  dvrelog  24820  xrlimcnp  25147  iedgedg  26398  edgiedgb  26402  edg0iedg0  26403  uhgrvtxedgiedgb  26484  uhgrvtxedgiedgbOLD  26485  uspgrf1oedg  26522  usgrf1oedg  26553  usgredg3  26562  ushgredgedg  26575  ushgredgedgloop  26577  ushgredgedgloopOLD  26578  usgrexmpledg  26609  0grsubgr  26625  uhgrspan1  26650  usgredgffibi  26671  dfnbgr3  26685  nbupgrres  26711  usgrnbcnvfv  26712  edginwlk  26982  wlkiswwlks2lem4  27221  wlkiswwlks2lem5  27222  clwlkclwwlk  27382  clwlkclwwlkOLD  27383  ex-rn  27872  bafval  28031  cnnvba  28106  minveco  28312  abrexexd  29909  imadifxp  29977  prsrn  30559  raddcn  30573  pl1cn  30599  esumrnmpt2  30728  sitgclbn  31003  mvtval  31996  elmsubrn  32024  dfon4  32589  ellines  32848  rnmptsn  33778  f1omptsnlem  33779  icoreresf  33795  ptrest  34018  ovoliunnfl  34061  voliunnfl  34063  rngoueqz  34347  rngonegmn1l  34348  rngonegmn1r  34349  rngoneglmul  34350  rngonegrmul  34351  zerdivemp1x  34354  isdrngo2  34365  rngokerinj  34382  iscrngo2  34404  idlnegcl  34429  1idl  34433  0rngo  34434  smprngopr  34459  prnc  34474  isfldidl  34475  isdmn3  34481  rncnvepres  34687  mzpmfp  38252  dmnonrel  38835  imanonrel  38838  cnvrcl0  38871  ntrrn  39358  rnresun  40267  disjinfi  40285  rnmpt0  40315  mptima  40336  imassmpt  40374  supxrleubrnmptf  40568  elicores  40650  limsupvaluz  40830  limsupmnflem  40842  limsupvaluz2  40860  limsup10ex  40895  liminf10ex  40896  liminflelimsuplem  40897  ioodvbdlimc1lem1  41056  ioodvbdlimc1  41058  ioodvbdlimc2  41060  fourierdlem42  41275  ioorrnopn  41431  subsaliuncl  41482  sge0sn  41502  sge0split  41532  sge0fodjrnlem  41539  sge0xaddlem2  41557  volicorescl  41676  hoidmvlelem3  41720  vonioolem2  41804  smflimsuplem1  41935  smflimsuplem3  41937  smflimsup  41943