Theorem rneqd 5920

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

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

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  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 5659  df-dm 5661  df-rn 5662

This theorem is used by:  elimampt  6035  imaeq1  6047  imaeq2  6048  resima2  6057  mptimass  6071  resiima  6074  rnxpid  6165  xpima  6174  imadifssranOLDOLD  6203  funimacnv  6621  fnima  6669  focofo  6809  rnfvprc  6879  elimampo  7557  elxp4  7934  elxp5  7935  2ndval  8004  fo2nd  8022  f2ndres  8026  curry1  8115  curry2  8118  oarec  8570  en1  9051  xpassen  9090  xpdom2  9091  sbthlem4  9109  fodomr  9147  fodomfir  9319  dffi3  9423  marypha2lem4  9430  ordtypelem9  9520  dfac12lem1  10222  dfac12r  10225  fin23lem32  10422  fin23lem34  10424  fin23lem35  10425  fin23lem36  10426  fin23lem38  10427  fin23lem39  10428  fin23lem41  10430  itunitc  10499  ttukeylem3  10589  fpwwe2lem5  10720  fpwwe2lem8  10723  wunex2  10823  wuncval2  10832  gruima  10887  rpnnen1lem6  13110  hashf1lem1  14600  s1rn  14746  swrdrn3  14802  s2rn  15116  s3rn  15117  s7rn  15118  relexprng  15199  relexprnd  15201  relexpfld  15202  limsupval  15641  vdwapfval  17149  vdwapval  17151  vdwmc  17156  vdwpc  17158  vdwlem6  17164  vdwlem8  17166  restval  17597  restid2  17601  prdsval  17626  prdsdsval  17649  prdsdsval2  17655  prdsdsval3  17656  imasval  17683  imasdsval  17687  isfull  18087  arwval  18218  gsumvalx  18865  conjsubg  19464  psgnfval  19714  sylow1lem2  19813  sylow1lem4  19815  sylow1  19817  sylow2blem1  19834  sylow2b  19837  sylow3lem1  19841  sylow3lem2  19842  sylow3lem3  19843  sylow3lem5  19845  sylow3lem6  19846  sylow3  19847  lsmfval  19852  lsmvalx  19853  oppglsm  19856  subglsm  19887  lsmpropd  19891  efgval2  19938  efgi2  19939  efgtlen  19940  efgsdm  19944  efgsdmi  19946  efgsrel  19948  efgs1b  19950  efgsp1  19951  efgsres  19952  efgsfo  19953  efgrelexlemb  19964  frgpnabllem1  20087  iscyg  20093  iscyggen  20094  gsumxp  20190  dprdval  20219  ablfac2  20305  zncyg  21854  cygznlem2a  21873  frlmsplit2  22079  evlseu  22392  tgrest  23477  ordtval  23507  ordtbas2  23509  ordtcnv  23519  ordtrest  23520  ordtrest2  23522  ispnrm  23657  cmpfi  23726  txval  23883  xkoval  23906  ptval2  23920  ptpjopn  23931  xkoccn  23938  xkoptsub  23973  xkopt  23974  fmval  24262  fmf  24264  txflf  24325  cnextf  24385  subgntr  24426  opnsubg  24427  clsnsg  24429  snclseqg  24435  tsmsval2  24449  tsmsxplem1  24472  ustuqtoplem  24558  utopsnneiplem  24566  utopsnneip  24567  fmucndlem  24609  ressprdsds  24690  mopnval  24757  metuval  24868  metdsval  25167  lebnumlem1  25282  lebnumlem3  25284  pi1xfrcnvlem  25377  pi1xfrcnv  25378  minveclem3b  25749  elovolmr  25797  ovolctb  25811  ovoliunlem3  25825  ovolshftlem1  25830  voliunlem3  25873  voliun  25875  volsup  25877  uniioombllem2  25904  uniioombllem3  25906  mbflimsup  25987  itg1climres  26035  itg2monolem1  26071  itg2i1fseq  26076  itg2cnlem1  26082  ellimc2  26197  dvivth  26330  dvne0  26331  lhop2  26335  lhop  26336  mdegfval  26380  dchrptlem2  27592  dchrpt  27594  seqsval  28674  om2noseqfo  28684  tglnunirn  29011  tgisline  29095  perpln1  29185  perpln2  29186  isperp  29187  ishpg  29237  tgplnfn  29253  plngval  29255  isplng  29256  lmif  29290  islmib  29292  cgrabasimass  29378  brprlng  29416  edgval  29627  edgopval  29629  edgstruct  29631  uhgr2edg  29789  usgr1e  29826  cplgrop  30018  cusgrexi  30024  structtocusgr  30027  1loopgredg  30082  1egrvtxdg0  30092  umgr2v2eedg  30105  ex-ima  31043  bafval  31206  pj3i  32810  ofrn2  33234  rnressnsn  33271  ffsrn  33320  prodindf  33429  pfxrn2  33507  pfxrn3  33508  swrdrn2  33517  gsumzresunsn  33623  gsumhashmul  33628  tocycfv  33670  tocycf  33678  trsp2cyc  33684  cycpmco2f1  33685  cycpmco2rn  33686  cycpmconjvlem  33702  cycpmconjslem2  33716  domnprodeq0  33840  qusbas2  33957  qusima  33959  qusrn  33960  nsgmgc  33963  nsgqusf1olem2  33965  idlsrgval  34035  esplyfval1  34205  esplyfvaln  34206  esplyind  34207  algextdeglem4  34352  smatrcl  34428  ordtprsval  34550  ordtprsuni  34551  ordtcnvNEW  34552  ordtrestNEW  34553  ordtrest2NEW  34555  qqhval  34604  qqhval2  34614  esumval  34678  esumsnf  34696  esumrnmpt2  34700  esumfsupre  34703  esumsup  34721  sxval  34823  omsval  34925  omsfval  34926  carsggect  34950  sibf0  34966  sitgfval  34973  cvmlift3lem6  36089  satfrnmapom  36135  mvtval  36265  mvrsval  36270  mrsubvrs  36287  elmsubrn  36293  msubrn  36294  mstaval  36309  msubvrs  36325  mclsval  36328  filnetlem4  37169  mptsnunlem  38261  dissneqlem  38263  exrecfnlem  38302  ctbssinf  38329  poimirlem3  38541  poimirlem9  38547  poimirlem16  38554  poimirlem17  38555  poimirlem19  38557  poimirlem20  38558  poimirlem24  38562  poimirlem30  38568  poimirlem32  38570  mblfinlem2  38576  ovoliunnfl  38580  voliunnfl  38582  isrngo  38831  drngoi  38885  rngohomval  38898  rngoisoval  38911  idlval  38947  pridlval  38967  maxidlval  38973  igenval  38995  cnvref4  39282  symrelim  39575  unidmqs  39671  lsatset  40047  docaffvalN  42178  docafvalN  42179  aks6d1c2  43180  sticksstones2  43197  sticksstones3  43198  qsalrel  43292  prjcrvfval  43667  mzpmfp  43757  eldiophb  43767  diophrw  43769  tfsconcatrn  44343  rp-tfslim  44354  conrel1d  44662  iunrelexp0  44701  rntrclfv  44731  clsneibex  45101  neicvgbex  45111  rnsnf  46198  fsneqrn  46223  limsupval3  46701  limsupresre  46705  limsupresico  46709  limsuppnfdlem  46710  limsupvaluz  46717  limsupvaluzmpt  46726  limsupvaluz2  46747  supcnvlimsup  46749  supcnvlimsupmpt  46750  liminfval  46768  liminfval5  46774  limsupresxr  46775  liminfresxr  46776  liminfresico  46780  liminfvalxr  46792  fourierdlem60  47175  fourierdlem61  47176  sge0val  47375  sge0z  47384  sge0revalmpt  47387  sge0tsms  47389  sge0sup  47400  sge0split  47418  sge0fodjrnlem  47425  sge0seq  47455  meadjiunlem  47474  meaiuninclem  47489  omeiunle  47526  ovolval2lem  47652  ovolval4lem2  47659  ovolval5lem2  47662  ovolval5lem3  47663  ovolval5  47664  ovnovollem2  47666  smfsuplem2  47821  smfsup  47823  smfsupmpt  47824  smfinf  47827  smfinfmpt  47828  smflimsuplem1  47829  smflimsuplem2  47830  smflimsuplem4  47832  smflimsuplem5  47833  smflimsuplem7  47835  smflimsup  47837  tmachlem-uassst  47952  fnrnafv  48231  afv2eq12d  48284  isubgredgss  48962  isubgredg  48963  stgredg  49053  gpgedg  49142  dmrnxp  49946  imaidfu  50217  idfudiag1lem  50630