Theorem rneqd 5923

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

Syntax hints:   → wi 4   = wceq 1540  ran crn 5660

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-cnv 5667  df-dm 5669  df-rn 5670

This theorem is referenced by:  resima2  6008  elimampt  6035  imaeq1  6047  imaeq2  6048  mptimass  6065  resiima  6068  imadifssran  6145  rnxpid  6167  xpima  6176  funimacnv  6622  fnima  6673  focofo  6808  rnfvprc  6875  elimampo  7549  elxp4  7923  elxp5  7924  2ndval  7996  fo2nd  8014  f2ndres  8018  curry1  8108  curry2  8111  oarec  8579  en1  9043  xpassen  9085  xpdom2  9086  sbthlem4  9105  fodomr  9147  fodomfir  9345  dffi3  9448  marypha2lem4  9455  ordtypelem9  9545  dfac12lem1  10163  dfac12r  10166  fin23lem32  10363  fin23lem34  10365  fin23lem35  10366  fin23lem36  10367  fin23lem38  10368  fin23lem39  10369  fin23lem41  10371  itunitc  10440  ttukeylem3  10530  fpwwe2lem5  10654  fpwwe2lem8  10657  wunex2  10757  wuncval2  10766  gruima  10821  rpnnen1lem6  13003  hashf1lem1  14478  s1rn  14622  s2rn  14987  s3rn  14988  s7rn  14989  relexprng  15070  relexprnd  15072  relexpfld  15073  limsupval  15495  vdwapfval  16996  vdwapval  16998  vdwmc  17003  vdwpc  17005  vdwlem6  17011  vdwlem8  17013  restval  17445  restid2  17449  prdsval  17474  prdsdsval  17497  prdsdsval2  17503  prdsdsval3  17504  imasval  17530  imasdsval  17534  isfull  17930  arwval  18061  gsumvalx  18659  conjsubg  19238  psgnfval  19486  sylow1lem2  19585  sylow1lem4  19587  sylow1  19589  sylow2blem1  19606  sylow2b  19609  sylow3lem1  19613  sylow3lem2  19614  sylow3lem3  19615  sylow3lem5  19617  sylow3lem6  19618  sylow3  19619  lsmfval  19624  lsmvalx  19625  oppglsm  19628  subglsm  19659  lsmpropd  19663  efgval2  19710  efgi2  19711  efgtlen  19712  efgsdm  19716  efgsdmi  19718  efgsrel  19720  efgs1b  19722  efgsp1  19723  efgsres  19724  efgsfo  19725  efgrelexlemb  19736  frgpnabllem1  19859  iscyg  19865  iscyggen  19866  gsumxp  19962  dprdval  19991  ablfac2  20077  zncyg  21514  cygznlem2a  21533  frlmsplit2  21738  evlseu  22046  tgrest  23102  ordtval  23132  ordtbas2  23134  ordtcnv  23144  ordtrest  23145  ordtrest2  23147  ispnrm  23282  cmpfi  23351  txval  23507  xkoval  23530  ptval2  23544  ptpjopn  23555  xkoccn  23562  xkoptsub  23597  xkopt  23598  fmval  23886  fmf  23888  txflf  23949  cnextf  24009  subgntr  24050  opnsubg  24051  clsnsg  24053  snclseqg  24059  tsmsval2  24073  tsmsxplem1  24096  ustuqtoplem  24183  utopsnneiplem  24191  utopsnneip  24192  fmucndlem  24234  ressprdsds  24315  mopnval  24382  metuval  24493  metdsval  24792  lebnumlem1  24916  lebnumlem3  24918  pi1xfrcnvlem  25012  pi1xfrcnv  25013  minveclem3b  25385  elovolmr  25434  ovolctb  25448  ovoliunlem3  25462  ovolshftlem1  25467  voliunlem3  25510  voliun  25512  volsup  25514  uniioombllem2  25541  uniioombllem3  25543  mbflimsup  25624  itg1climres  25672  itg2monolem1  25708  itg2i1fseq  25713  itg2cnlem1  25719  ellimc2  25835  dvivth  25972  dvne0  25973  lhop2  25977  lhop  25978  mdegfval  26024  dchrptlem2  27233  dchrpt  27235  seqsval  28239  om2noseqfo  28249  tglnunirn  28532  tgisline  28611  perpln1  28694  perpln2  28695  isperp  28696  ishpg  28743  lmif  28769  islmib  28771  edgval  29033  edgopval  29035  edgstruct  29037  uhgr2edg  29192  usgr1e  29229  cplgrop  29421  cusgrexi  29427  structtocusgr  29430  1loopgredg  29486  1egrvtxdg0  29496  umgr2v2eedg  29509  ex-ima  30428  bafval  30590  pj3i  32194  ofrn2  32623  ffsrn  32711  prodindf  32845  pfxrn2  32920  pfxrn3  32921  swrdrn2  32935  swrdrn3  32936  gsumzresunsn  33055  gsumhashmul  33060  tocycfv  33125  tocycf  33133  trsp2cyc  33139  cycpmco2f1  33140  cycpmco2rn  33141  cycpmconjvlem  33157  cycpmconjslem2  33171  qusbas2  33426  qusima  33428  qusrn  33429  nsgmgc  33432  nsgqusf1olem2  33434  idlsrgval  33523  algextdeglem4  33759  smatrcl  33832  ordtprsval  33954  ordtprsuni  33955  ordtcnvNEW  33956  ordtrestNEW  33957  ordtrest2NEW  33959  qqhval  34008  qqhval2  34018  esumval  34082  esumsnf  34100  esumrnmpt2  34104  esumfsupre  34107  esumsup  34125  sxval  34226  omsval  34330  omsfval  34331  carsggect  34355  sibf0  34371  sitgfval  34378  cvmlift3lem6  35351  satfrnmapom  35397  mvtval  35527  mvrsval  35532  mrsubvrs  35549  elmsubrn  35555  msubrn  35556  mstaval  35571  msubvrs  35587  mclsval  35590  filnetlem4  36404  mptsnunlem  37361  dissneqlem  37363  exrecfnlem  37402  ctbssinf  37429  poimirlem3  37652  poimirlem9  37658  poimirlem16  37665  poimirlem17  37666  poimirlem19  37668  poimirlem20  37669  poimirlem24  37673  poimirlem30  37679  poimirlem32  37681  mblfinlem2  37687  ovoliunnfl  37691  voliunnfl  37693  isrngo  37926  drngoi  37980  rngohomval  37993  rngoisoval  38006  idlval  38042  pridlval  38062  maxidlval  38068  igenval  38090  cnvref4  38373  symrelim  38582  unidmqs  38677  lsatset  39013  docaffvalN  41145  docafvalN  41146  aks6d1c2  42148  sticksstones2  42165  sticksstones3  42166  qsalrel  42258  prjcrvfval  42629  mzpmfp  42745  eldiophb  42755  diophrw  42757  tfsconcatrn  43341  rp-tfslim  43352  conrel1d  43662  iunrelexp0  43701  rntrclfv  43731  clsneibex  44101  neicvgbex  44111  rnsnf  45188  fsneqrn  45215  limsupval3  45701  limsupresre  45705  limsupresico  45709  limsuppnfdlem  45710  limsupvaluz  45717  limsupvaluzmpt  45726  limsupvaluz2  45747  supcnvlimsup  45749  supcnvlimsupmpt  45750  liminfval  45768  liminfval5  45774  limsupresxr  45775  liminfresxr  45776  liminfresico  45780  liminfvalxr  45792  fourierdlem60  46175  fourierdlem61  46176  sge0val  46375  sge0z  46384  sge0revalmpt  46387  sge0tsms  46389  sge0sup  46400  sge0split  46418  sge0fodjrnlem  46425  sge0seq  46455  meadjiunlem  46474  meaiuninclem  46489  omeiunle  46526  ovolval2lem  46652  ovolval4lem2  46659  ovolval5lem2  46662  ovolval5lem3  46663  ovolval5  46664  ovnovollem2  46666  smfsuplem2  46821  smfsup  46823  smfsupmpt  46824  smfinf  46827  smfinfmpt  46828  smflimsuplem1  46829  smflimsuplem2  46830  smflimsuplem4  46832  smflimsuplem5  46833  smflimsuplem7  46835  smflimsup  46837  fnrnafv  47171  afv2eq12d  47224  isubgredgss  47858  isubgredg  47859  stgredg  47948  gpgedg  48029  dmrnxp  48795  imaidfu  49049  idfudiag1lem  49388