Theorem rneqd 5922

Description: Equality deduction for range. (Contributed by NM, 4-Mar-2004.)

Hypothesis

Ref	Expression
rneqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
rneqd	⊢ (𝜑 → ran 𝐴 = ran 𝐵)

Proof of Theorem rneqd

Step	Hyp	Ref	Expression
1		rneqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		rneq 5920	. 2 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
3	1, 2	syl 18	1 ⊢ (𝜑 → ran 𝐴 = ran 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ran crn 5656

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

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 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-cnv 5663  df-dm 5665  df-rn 5666

This theorem is used by:  resima2  6009  elimampt  6039  imaeq1  6051  imaeq2  6052  mptimass  6069  resiima  6072  rnxpid  6166  xpima  6175  imadifssranOLD  6198  funimacnv  6615  fnima  6663  focofo  6803  rnfvprc  6873  elimampo  7551  elxp4  7920  elxp5  7921  2ndval  7990  fo2nd  8008  f2ndres  8012  curry1  8102  curry2  8105  oarec  8550  en1  9031  xpassen  9070  xpdom2  9071  sbthlem4  9089  fodomr  9127  fodomfir  9298  dffi3  9402  marypha2lem4  9409  ordtypelem9  9499  dfac12lem1  10147  dfac12r  10150  fin23lem32  10347  fin23lem34  10349  fin23lem35  10350  fin23lem36  10351  fin23lem38  10352  fin23lem39  10353  fin23lem41  10355  itunitc  10424  ttukeylem3  10514  fpwwe2lem5  10645  fpwwe2lem8  10648  wunex2  10748  wuncval2  10757  gruima  10812  rpnnen1lem6  13033  hashf1lem1  14521  s1rn  14667  swrdrn3  14723  s2rn  15037  s3rn  15038  s7rn  15039  relexprng  15120  relexprnd  15122  relexpfld  15123  limsupval  15562  vdwapfval  17064  vdwapval  17066  vdwmc  17071  vdwpc  17073  vdwlem6  17079  vdwlem8  17081  restval  17512  restid2  17516  prdsval  17541  prdsdsval  17564  prdsdsval2  17570  prdsdsval3  17571  imasval  17598  imasdsval  17602  isfull  18002  arwval  18133  gsumvalx  18779  conjsubg  19378  psgnfval  19628  sylow1lem2  19727  sylow1lem4  19729  sylow1  19731  sylow2blem1  19748  sylow2b  19751  sylow3lem1  19755  sylow3lem2  19756  sylow3lem3  19757  sylow3lem5  19759  sylow3lem6  19760  sylow3  19761  lsmfval  19766  lsmvalx  19767  oppglsm  19770  subglsm  19801  lsmpropd  19805  efgval2  19852  efgi2  19853  efgtlen  19854  efgsdm  19858  efgsdmi  19860  efgsrel  19862  efgs1b  19864  efgsp1  19865  efgsres  19866  efgsfo  19867  efgrelexlemb  19878  frgpnabllem1  20001  iscyg  20007  iscyggen  20008  gsumxp  20104  dprdval  20133  ablfac2  20219  zncyg  21762  cygznlem2a  21781  frlmsplit2  21987  evlseu  22300  tgrest  23385  ordtval  23415  ordtbas2  23417  ordtcnv  23427  ordtrest  23428  ordtrest2  23430  ispnrm  23565  cmpfi  23634  txval  23791  xkoval  23814  ptval2  23828  ptpjopn  23839  xkoccn  23846  xkoptsub  23881  xkopt  23882  fmval  24170  fmf  24172  txflf  24233  cnextf  24293  subgntr  24334  opnsubg  24335  clsnsg  24337  snclseqg  24343  tsmsval2  24357  tsmsxplem1  24380  ustuqtoplem  24466  utopsnneiplem  24474  utopsnneip  24475  fmucndlem  24517  ressprdsds  24598  mopnval  24665  metuval  24776  metdsval  25075  lebnumlem1  25190  lebnumlem3  25192  pi1xfrcnvlem  25285  pi1xfrcnv  25286  minveclem3b  25657  elovolmr  25705  ovolctb  25719  ovoliunlem3  25733  ovolshftlem1  25738  voliunlem3  25781  voliun  25783  volsup  25785  uniioombllem2  25812  uniioombllem3  25814  mbflimsup  25895  itg1climres  25943  itg2monolem1  25979  itg2i1fseq  25984  itg2cnlem1  25990  ellimc2  26105  dvivth  26238  dvne0  26239  lhop2  26243  lhop  26244  mdegfval  26288  dchrptlem2  27502  dchrpt  27504  seqsval  28554  om2noseqfo  28564  tglnunirn  28891  tgisline  28975  perpln1  29065  perpln2  29066  isperp  29067  ishpg  29117  tgplnfn  29133  plngval  29135  isplng  29136  lmif  29170  islmib  29172  cgrabasimass  29258  brprlng  29296  edgval  29507  edgopval  29509  edgstruct  29511  uhgr2edg  29669  usgr1e  29706  cplgrop  29898  cusgrexi  29904  structtocusgr  29907  1loopgredg  29962  1egrvtxdg0  29972  umgr2v2eedg  29985  ex-ima  30923  bafval  31086  pj3i  32690  ofrn2  33114  rnressnsn  33151  ffsrn  33200  prodindf  33309  pfxrn2  33387  pfxrn3  33388  swrdrn2  33397  gsumzresunsn  33503  gsumhashmul  33508  tocycfv  33550  tocycf  33558  trsp2cyc  33564  cycpmco2f1  33565  cycpmco2rn  33566  cycpmconjvlem  33582  cycpmconjslem2  33596  domnprodeq0  33720  qusbas2  33836  qusima  33838  qusrn  33839  nsgmgc  33842  nsgqusf1olem2  33844  idlsrgval  33914  esplyfval1  34084  esplyfvaln  34085  esplyind  34086  algextdeglem4  34231  smatrcl  34307  ordtprsval  34429  ordtprsuni  34430  ordtcnvNEW  34431  ordtrestNEW  34432  ordtrest2NEW  34434  qqhval  34483  qqhval2  34493  esumval  34557  esumsnf  34575  esumrnmpt2  34579  esumfsupre  34582  esumsup  34600  sxval  34702  omsval  34805  omsfval  34806  carsggect  34830  sibf0  34846  sitgfval  34853  cvmlift3lem6  35904  satfrnmapom  35950  mvtval  36080  mvrsval  36085  mrsubvrs  36102  elmsubrn  36108  msubrn  36109  mstaval  36124  msubvrs  36140  mclsval  36143  filnetlem4  37001  mptsnunlem  38093  dissneqlem  38095  exrecfnlem  38134  ctbssinf  38161  poimirlem3  38373  poimirlem9  38379  poimirlem16  38386  poimirlem17  38387  poimirlem19  38389  poimirlem20  38390  poimirlem24  38394  poimirlem30  38400  poimirlem32  38402  mblfinlem2  38408  ovoliunnfl  38412  voliunnfl  38414  isrngo  38648  drngoi  38702  rngohomval  38715  rngoisoval  38728  idlval  38764  pridlval  38784  maxidlval  38790  igenval  38812  cnvref4  39099  symrelim  39392  unidmqs  39488  lsatset  39864  docaffvalN  41995  docafvalN  41996  aks6d1c2  42997  sticksstones2  43014  sticksstones3  43015  qsalrel  43109  prjcrvfval  43478  mzpmfp  43593  eldiophb  43603  diophrw  43605  tfsconcatrn  44184  rp-tfslim  44195  conrel1d  44504  iunrelexp0  44543  rntrclfv  44573  clsneibex  44943  neicvgbex  44953  rnsnf  46017  fsneqrn  46042  limsupval3  46521  limsupresre  46525  limsupresico  46529  limsuppnfdlem  46530  limsupvaluz  46537  limsupvaluzmpt  46546  limsupvaluz2  46567  supcnvlimsup  46569  supcnvlimsupmpt  46570  liminfval  46588  liminfval5  46594  limsupresxr  46595  liminfresxr  46596  liminfresico  46600  liminfvalxr  46612  fourierdlem60  46995  fourierdlem61  46996  sge0val  47195  sge0z  47204  sge0revalmpt  47207  sge0tsms  47209  sge0sup  47220  sge0split  47238  sge0fodjrnlem  47245  sge0seq  47275  meadjiunlem  47294  meaiuninclem  47309  omeiunle  47346  ovolval2lem  47472  ovolval4lem2  47479  ovolval5lem2  47482  ovolval5lem3  47483  ovolval5  47484  ovnovollem2  47486  smfsuplem2  47641  smfsup  47643  smfsupmpt  47644  smfinf  47647  smfinfmpt  47648  smflimsuplem1  47649  smflimsuplem2  47650  smflimsuplem4  47652  smflimsuplem5  47653  smflimsuplem7  47655  smflimsup  47657  tmachlem-uassst  47772  fnrnafv  48051  afv2eq12d  48104  isubgredgss  48782  isubgredg  48783  stgredg  48873  gpgedg  48962  dmrnxp  49766  imaidfu  50037  idfudiag1lem  50450