Theorem rneqd 5921

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 5919	. 2 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
3	1, 2	syl 18	1 ⊢ (𝜑 → ran 𝐴 = ran 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ran crn 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-cnv 5659  df-dm 5661  df-rn 5662

This theorem is used by:  elimampt  6037  imaeq1  6049  imaeq2  6050  resima2  6059  mptimass  6073  resiima  6076  rnxpid  6167  xpima  6176  imadifssranOLDOLD  6206  funimacnv  6626  fnima  6674  focofo  6814  rnfvprc  6884  elimampo  7561  elxp4  7938  elxp5  7939  2ndval  8008  fo2nd  8026  f2ndres  8030  curry1  8122  curry2  8125  oarec  8578  en1  9059  xpassen  9098  xpdom2  9099  sbthlem4  9117  fodomr  9155  fodomfir  9327  dffi3  9430  marypha2lem4  9437  ordtypelem9  9527  dfac12lem1  10229  dfac12r  10232  fin23lem32  10429  fin23lem34  10431  fin23lem35  10432  fin23lem36  10433  fin23lem38  10434  fin23lem39  10435  fin23lem41  10437  itunitc  10506  ttukeylem3  10596  fpwwe2lem5  10727  fpwwe2lem8  10730  wunex2  10830  wuncval2  10839  gruima  10894  rpnnen1lem6  13117  hashf1lem1  14607  s1rn  14753  swrdrn3  14810  s2rn  15125  s3rn  15126  s7rn  15127  relexprng  15208  relexprnd  15210  relexpfld  15211  limsupval  15650  vdwapfval  17158  vdwapval  17160  vdwmc  17165  vdwpc  17167  vdwlem6  17173  vdwlem8  17175  restval  17606  restid2  17610  prdsval  17635  prdsdsval  17658  prdsdsval2  17664  prdsdsval3  17665  imasval  17692  imasdsval  17696  isfull  18096  arwval  18227  gsumvalx  18874  conjsubg  19473  psgnfval  19723  sylow1lem2  19822  sylow1lem4  19824  sylow1  19826  sylow2blem1  19843  sylow2b  19846  sylow3lem1  19850  sylow3lem2  19851  sylow3lem3  19852  sylow3lem5  19854  sylow3lem6  19855  sylow3  19856  lsmfval  19861  lsmvalx  19862  oppglsm  19865  subglsm  19896  lsmpropd  19900  efgval2  19947  efgi2  19948  efgtlen  19949  efgsdm  19953  efgsdmi  19955  efgsrel  19957  efgs1b  19959  efgsp1  19960  efgsres  19961  efgsfo  19962  efgrelexlemb  19973  frgpnabllem1  20096  iscyg  20102  iscyggen  20103  gsumxp  20199  dprdval  20228  ablfac2  20314  zncyg  21863  cygznlem2a  21882  frlmsplit2  22088  evlseu  22401  tgrest  23486  ordtval  23516  ordtbas2  23518  ordtcnv  23528  ordtrest  23529  ordtrest2  23531  ispnrm  23666  cmpfi  23735  txval  23892  xkoval  23915  ptval2  23929  ptpjopn  23940  xkoccn  23947  xkoptsub  23982  xkopt  23983  fmval  24271  fmf  24273  txflf  24334  cnextf  24394  subgntr  24435  opnsubg  24436  clsnsg  24438  snclseqg  24444  tsmsval2  24458  tsmsxplem1  24481  ustuqtoplem  24567  utopsnneiplem  24575  utopsnneip  24576  fmucndlem  24618  ressprdsds  24699  mopnval  24766  metuval  24877  metdsval  25176  lebnumlem1  25291  lebnumlem3  25293  pi1xfrcnvlem  25386  pi1xfrcnv  25387  minveclem3b  25758  elovolmr  25806  ovolctb  25820  ovoliunlem3  25834  ovolshftlem1  25839  voliunlem3  25882  voliun  25884  volsup  25886  uniioombllem2  25913  uniioombllem3  25915  mbflimsup  25996  itg1climres  26044  itg2monolem1  26080  itg2i1fseq  26085  itg2cnlem1  26091  ellimc2  26206  dvivth  26339  dvne0  26340  lhop2  26344  lhop  26345  mdegfval  26389  dchrptlem2  27601  dchrpt  27603  seqsval  28683  om2noseqfo  28693  tglnunirn  29020  tgisline  29104  perpln1  29194  perpln2  29195  isperp  29196  ishpg  29246  tgplnfn  29262  plngval  29264  isplng  29265  lmif  29299  islmib  29301  cgrabasimass  29387  brprlng  29425  edgval  29636  edgopval  29638  edgstruct  29640  uhgr2edg  29798  usgr1e  29835  cplgrop  30027  cusgrexi  30033  structtocusgr  30036  1loopgredg  30091  1egrvtxdg0  30101  umgr2v2eedg  30114  ex-ima  31052  bafval  31215  pj3i  32819  ofrn2  33285  rnressnsn  33322  ffsrn  33370  prodindf  33479  pfxrn2  33557  pfxrn3  33558  swrdrn2  33567  gsumzresunsn  33673  gsumhashmul  33678  tocycfv  33720  tocycf  33728  trsp2cyc  33734  cycpmco2f1  33735  cycpmco2rn  33736  cycpmconjvlem  33752  cycpmconjslem2  33766  domnprodeq0  33890  qusbas2  34007  qusima  34009  qusrn  34010  nsgmgc  34013  nsgqusf1olem2  34015  idlsrgval  34085  esplyfval1  34255  esplyfvaln  34256  esplyind  34257  algextdeglem4  34402  smatrcl  34478  ordtprsval  34600  ordtprsuni  34601  ordtcnvNEW  34602  ordtrestNEW  34603  ordtrest2NEW  34605  qqhval  34654  qqhval2  34664  esumval  34728  esumsnf  34746  esumrnmpt2  34750  esumfsupre  34753  esumsup  34771  sxval  34873  omsval  34975  omsfval  34976  carsggect  35000  sibf0  35016  sitgfval  35023  cvmlift3lem6  36207  satfrnmapom  36253  mvtval  36383  mvrsval  36388  mrsubvrs  36405  elmsubrn  36411  msubrn  36412  mstaval  36427  msubvrs  36443  mclsval  36446  filnetlem4  37293  mptsnunlem  38398  dissneqlem  38400  exrecfnlem  38439  ctbssinf  38466  poimirlem3  38678  poimirlem9  38684  poimirlem16  38691  poimirlem17  38692  poimirlem19  38694  poimirlem20  38695  poimirlem24  38699  poimirlem30  38705  poimirlem32  38707  mblfinlem2  38713  ovoliunnfl  38717  voliunnfl  38719  isrngo  38968  drngoi  39022  rngohomval  39035  rngoisoval  39048  idlval  39084  pridlval  39104  maxidlval  39110  igenval  39132  cnvref4  39419  symrelim  39712  unidmqs  39808  lsatset  40184  docaffvalN  42315  docafvalN  42316  aks6d1c2  43317  sticksstones2  43334  sticksstones3  43335  qsalrel  43429  prjcrvfval  43804  mzpmfp  43895  eldiophb  43905  diophrw  43907  tfsconcatrn  44481  rp-tfslim  44492  conrel1d  44800  iunrelexp0  44839  rntrclfv  44869  clsneibex  45239  neicvgbex  45249  rnsnf  46335  fsneqrn  46360  limsupval3  46838  limsupresre  46842  limsupresico  46846  limsuppnfdlem  46847  limsupvaluz  46854  limsupvaluzmpt  46863  limsupvaluz2  46884  supcnvlimsup  46886  supcnvlimsupmpt  46887  liminfval  46905  liminfval5  46911  limsupresxr  46912  liminfresxr  46913  liminfresico  46917  liminfvalxr  46929  fourierdlem60  47312  fourierdlem61  47313  sge0val  47512  sge0z  47521  sge0revalmpt  47524  sge0tsms  47526  sge0sup  47537  sge0split  47555  sge0fodjrnlem  47562  sge0seq  47592  meadjiunlem  47611  meaiuninclem  47626  omeiunle  47663  ovolval2lem  47789  ovolval4lem2  47796  ovolval5lem2  47799  ovolval5lem3  47800  ovolval5  47801  ovnovollem2  47803  smfsuplem2  47958  smfsup  47960  smfsupmpt  47961  smfinf  47964  smfinfmpt  47965  smflimsuplem1  47966  smflimsuplem2  47967  smflimsuplem4  47969  smflimsuplem5  47970  smflimsuplem7  47972  smflimsup  47974  tmachlem-uassst  48089  fnrnafv  48368  afv2eq12d  48421  isubgredgss  49099  isubgredg  49100  stgredg  49190  gpgedg  49279  dmrnxp  50084  imaidfu  50362  idfudiag1lem  50794