Theorem rneqd 5598

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

Syntax hints:   → wi 4   = 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 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

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 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4887  df-opab 4949  df-cnv 5363  df-dm 5365  df-rn 5366

This theorem is referenced by:  resima2  5681  imaeq1  5715  imaeq2  5716  resiima  5734  rnxpid  5821  xpima  5830  funimacnv  6215  fnima  6256  rnfvprc  6440  elxp4  7389  elxp5  7390  2ndval  7448  fo2nd  7466  f2ndres  7470  curry1  7550  curry2  7553  oarec  7926  en1  8308  xpassen  8342  xpdom2  8343  sbthlem4  8361  fodomr  8399  dffi3  8625  marypha2lem4  8632  ordtypelem9  8720  dfac12lem1  9300  dfac12r  9303  fin23lem32  9501  fin23lem34  9503  fin23lem35  9504  fin23lem36  9505  fin23lem38  9506  fin23lem39  9507  fin23lem41  9509  itunitc  9578  ttukeylem3  9668  fpwwe2lem6  9792  fpwwe2lem9  9795  wunex2  9895  wuncval2  9904  gruima  9959  rpnnen1lem6  12129  hashf1lem1  13553  s1rn  13689  relexprng  14193  relexpfld  14196  limsupval  14613  vdwapfval  16079  vdwapval  16081  vdwmc  16086  vdwpc  16088  vdwlem6  16094  vdwlem8  16096  restval  16473  restid2  16477  prdsval  16501  prdsdsval  16524  prdsdsval2  16530  prdsdsval3  16531  imasval  16557  imasdsval  16561  isfull  16955  arwval  17078  gsumvalx  17656  conjsubg  18076  psgnfval  18304  sylow1lem2  18398  sylow1lem4  18400  sylow1  18402  sylow2blem1  18419  sylow2b  18422  sylow3lem1  18426  sylow3lem2  18427  sylow3lem3  18428  sylow3lem5  18430  sylow3lem6  18431  sylow3  18432  lsmfval  18437  lsmvalx  18438  oppglsm  18441  subglsm  18470  lsmpropd  18474  efgval2  18521  efgi2  18522  efgtlen  18523  efgsdm  18527  efgsdmi  18529  efgsrel  18531  efgs1b  18533  efgsp1  18534  efgsres  18535  efgsresOLD  18536  efgsfo  18537  efgrelexlemb  18549  frgpnabllem1  18662  iscyg  18667  iscyggen  18668  gsumxp  18761  dprdval  18789  ablfac2  18875  evlseu  19912  zncyg  20292  cygznlem2a  20311  frlmsplit2  20516  tgrest  21371  ordtval  21401  ordtbas2  21403  ordtcnv  21413  ordtrest  21414  ordtrest2  21416  ispnrm  21551  cmpfi  21620  txval  21776  xkoval  21799  ptval2  21813  ptpjopn  21824  xkoccn  21831  xkoptsub  21866  xkopt  21867  fmval  22155  fmf  22157  txflf  22218  cnextf  22278  subgntr  22318  opnsubg  22319  clsnsg  22321  snclseqg  22327  tsmsval2  22341  tsmsxplem1  22364  ustuqtoplem  22451  utopsnneiplem  22459  utopsnneip  22460  fmucndlem  22503  ressprdsds  22584  mopnval  22651  metuval  22762  metdsval  23058  lebnumlem1  23168  lebnumlem3  23170  pi1xfrcnvlem  23263  pi1xfrcnv  23264  minveclem3b  23634  elovolmr  23680  ovolctb  23694  ovoliunlem3  23708  ovolshftlem1  23713  voliunlem3  23756  voliun  23758  volsup  23760  uniioombllem2  23787  uniioombllem3  23789  mbflimsup  23870  itg1climres  23918  itg2monolem1  23954  itg2i1fseq  23959  itg2cnlem1  23965  ellimc2  24078  dvivth  24210  dvne0  24211  lhop2  24215  lhop  24216  mdegfval  24259  dchrptlem2  25442  dchrpt  25444  tglnunirn  25899  tgisline  25978  perpln1  26061  perpln2  26062  isperp  26063  ishpg  26107  lmif  26133  islmib  26135  edgval  26397  edgopval  26399  edgstruct  26401  uhgr2edg  26554  usgr1e  26592  cplgrop  26785  cusgrexi  26791  structtocusgr  26794  1loopgredg  26849  1egrvtxdg0  26859  umgr2v2eedg  26872  ex-ima  27874  bafval  28031  pj3i  29639  elimampt  30003  ofrn2  30007  ffsrn  30070  smatrcl  30460  ordtprsval  30562  ordtprsuni  30563  ordtcnvNEW  30564  ordtrestNEW  30565  ordtrest2NEW  30567  qqhval  30616  qqhval2  30624  prodindf  30683  esumval  30706  esumsnf  30724  esumrnmpt2  30728  esumfsupre  30731  esumsup  30749  sxval  30851  omsval  30953  omsfval  30954  carsggect  30978  sibf0  30994  sitgfval  31001  cvmlift3lem6  31905  mvtval  31996  mvrsval  32001  mrsubvrs  32018  elmsubrn  32024  msubrn  32025  mstaval  32040  msubvrs  32056  mclsval  32059  trpredeq1  32308  trpredeq2  32309  trpredeq3  32310  filnetlem4  32964  mptsnunlem  33781  dissneqlem  33783  poimirlem3  34038  poimirlem9  34044  poimirlem16  34051  poimirlem17  34052  poimirlem19  34054  poimirlem20  34055  poimirlem24  34059  poimirlem30  34065  poimirlem32  34067  mblfinlem2  34073  ovoliunnfl  34077  voliunnfl  34079  isrngo  34320  drngoi  34374  rngohomval  34387  rngoisoval  34400  idlval  34436  pridlval  34456  maxidlval  34462  igenval  34484  symrelim  34933  lsatset  35144  docaffvalN  37275  docafvalN  37276  mzpmfp  38270  eldiophb  38280  diophrw  38282  conrel1d  38912  iunrelexp0  38951  rntrclfv  38981  clsneibex  39356  neicvgbex  39366  rnsnf  40293  fsneqrn  40324  mptima2  40370  limsupval3  40832  limsupresre  40836  limsupresico  40840  limsuppnfdlem  40841  limsupvaluz  40848  limsupvaluzmpt  40857  limsupvaluz2  40878  supcnvlimsup  40880  supcnvlimsupmpt  40881  liminfval  40899  liminfval5  40905  limsupresxr  40906  liminfresxr  40907  liminfresico  40911  liminfvalxr  40923  fourierdlem60  41310  fourierdlem61  41311  sge0val  41507  sge0z  41516  sge0revalmpt  41519  sge0tsms  41521  sge0sup  41532  sge0split  41550  sge0fodjrnlem  41557  sge0seq  41587  meadjiunlem  41606  meaiuninclem  41621  omeiunle  41658  ovolval2lem  41784  ovolval4lem2  41791  ovolval5lem2  41794  ovolval5lem3  41795  ovolval5  41796  ovnovollem2  41798  smfsuplem2  41945  smfsup  41947  smfsupmpt  41948  smfinf  41951  smfinfmpt  41952  smflimsuplem1  41953  smflimsuplem2  41954  smflimsuplem4  41956  smflimsuplem5  41957  smflimsuplem7  41959  smflimsup  41961  fnrnafv  42203  afv2eq12d  42256