Theorem rneqd 5914

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

Syntax hints:   → wi 4   = wceq 1560  ran crn 5648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-cnv 5655  df-dm 5657  df-rn 5658

This theorem is referenced by:  resima2  6002  elimampt  6032  imaeq1  6044  imaeq2  6045  mptimass  6062  resiima  6065  imadifssran  6136  rnxpid  6159  xpima  6168  funimacnv  6602  fnima  6651  focofo  6791  rnfvprc  6861  elimampo  7533  elxp4  7903  elxp5  7904  2ndval  7973  fo2nd  7991  f2ndres  7995  curry1  8083  curry2  8086  oarec  8531  en1  9005  xpassen  9043  xpdom2  9044  sbthlem4  9062  fodomr  9100  fodomfir  9272  dffi3  9377  marypha2lem4  9384  ordtypelem9  9474  dfac12lem1  10100  dfac12r  10103  fin23lem32  10301  fin23lem34  10303  fin23lem35  10304  fin23lem36  10305  fin23lem38  10306  fin23lem39  10307  fin23lem41  10309  itunitc  10378  ttukeylem3  10468  fpwwe2lem5  10593  fpwwe2lem8  10596  wunex2  10696  wuncval2  10705  gruima  10760  rpnnen1lem6  12983  hashf1lem1  14468  s1rn  14613  s2rn  14976  s3rn  14977  s7rn  14978  relexprng  15059  relexprnd  15061  relexpfld  15062  limsupval  15501  vdwapfval  17007  vdwapval  17009  vdwmc  17014  vdwpc  17016  vdwlem6  17022  vdwlem8  17024  restval  17455  restid2  17459  prdsval  17484  prdsdsval  17507  prdsdsval2  17513  prdsdsval3  17514  imasval  17541  imasdsval  17545  isfull  17945  arwval  18076  gsumvalx  18710  conjsubg  19290  psgnfval  19540  sylow1lem2  19639  sylow1lem4  19641  sylow1  19643  sylow2blem1  19660  sylow2b  19663  sylow3lem1  19667  sylow3lem2  19668  sylow3lem3  19669  sylow3lem5  19671  sylow3lem6  19672  sylow3  19673  lsmfval  19678  lsmvalx  19679  oppglsm  19682  subglsm  19713  lsmpropd  19717  efgval2  19764  efgi2  19765  efgtlen  19766  efgsdm  19770  efgsdmi  19772  efgsrel  19774  efgs1b  19776  efgsp1  19777  efgsres  19778  efgsfo  19779  efgrelexlemb  19790  frgpnabllem1  19913  iscyg  19919  iscyggen  19920  gsumxp  20016  dprdval  20045  ablfac2  20131  zncyg  21600  cygznlem2a  21619  frlmsplit2  21825  evlseu  22136  tgrest  23219  ordtval  23249  ordtbas2  23251  ordtcnv  23261  ordtrest  23262  ordtrest2  23264  ispnrm  23399  cmpfi  23468  txval  23624  xkoval  23647  ptval2  23661  ptpjopn  23672  xkoccn  23679  xkoptsub  23714  xkopt  23715  fmval  24003  fmf  24005  txflf  24066  cnextf  24126  subgntr  24167  opnsubg  24168  clsnsg  24170  snclseqg  24176  tsmsval2  24190  tsmsxplem1  24213  ustuqtoplem  24299  utopsnneiplem  24307  utopsnneip  24308  fmucndlem  24350  ressprdsds  24431  mopnval  24498  metuval  24609  metdsval  24908  lebnumlem1  25023  lebnumlem3  25025  pi1xfrcnvlem  25118  pi1xfrcnv  25119  minveclem3b  25490  elovolmr  25538  ovolctb  25552  ovoliunlem3  25566  ovolshftlem1  25571  voliunlem3  25614  voliun  25616  volsup  25618  uniioombllem2  25645  uniioombllem3  25647  mbflimsup  25728  itg1climres  25776  itg2monolem1  25812  itg2i1fseq  25817  itg2cnlem1  25823  ellimc2  25939  dvivth  26072  dvne0  26073  lhop2  26077  lhop  26078  mdegfval  26122  dchrptlem2  27329  dchrpt  27331  seqsval  28381  om2noseqfo  28391  tglnunirn  28717  tgisline  28796  perpln1  28883  perpln2  28884  isperp  28885  ishpg  28932  lmif  28958  islmib  28960  tgplnfn  28982  plngval  28984  isplng  28985  brprlng  29065  edgval  29250  edgopval  29252  edgstruct  29254  uhgr2edg  29409  usgr1e  29446  cplgrop  29638  cusgrexi  29644  structtocusgr  29647  1loopgredg  29702  1egrvtxdg0  29712  umgr2v2eedg  29725  ex-ima  30644  bafval  30807  pj3i  32411  ofrn2  32842  rnressnsn  32879  ffsrn  32930  prodindf  33040  pfxrn2  33118  pfxrn3  33119  swrdrn2  33132  swrdrn3  33133  gsumzresunsn  33242  gsumhashmul  33247  tocycfv  33289  tocycf  33297  trsp2cyc  33303  cycpmco2f1  33304  cycpmco2rn  33305  cycpmconjvlem  33321  cycpmconjslem2  33335  domnprodeq0  33460  qusbas2  33592  qusima  33594  qusrn  33595  nsgmgc  33598  nsgqusf1olem2  33600  idlsrgval  33699  esplyfval1  33870  esplyfvaln  33871  esplyind  33872  algextdeglem4  34017  smatrcl  34093  ordtprsval  34215  ordtprsuni  34216  ordtcnvNEW  34217  ordtrestNEW  34218  ordtrest2NEW  34220  qqhval  34269  qqhval2  34279  esumval  34343  esumsnf  34361  esumrnmpt2  34365  esumfsupre  34368  esumsup  34386  sxval  34487  omsval  34590  omsfval  34591  carsggect  34615  sibf0  34631  sitgfval  34638  cvmlift3lem6  35674  satfrnmapom  35720  mvtval  35850  mvrsval  35855  mrsubvrs  35872  elmsubrn  35878  msubrn  35879  mstaval  35894  msubvrs  35910  mclsval  35913  filnetlem4  36741  mptsnunlem  37832  dissneqlem  37834  exrecfnlem  37873  ctbssinf  37900  poimirlem3  38122  poimirlem9  38128  poimirlem16  38135  poimirlem17  38136  poimirlem19  38138  poimirlem20  38139  poimirlem24  38143  poimirlem30  38149  poimirlem32  38151  mblfinlem2  38157  ovoliunnfl  38161  voliunnfl  38163  isrngo  38396  drngoi  38450  rngohomval  38463  rngoisoval  38476  idlval  38512  pridlval  38532  maxidlval  38538  igenval  38560  cnvref4  38849  symrelim  39142  unidmqs  39238  lsatset  39614  docaffvalN  41745  docafvalN  41746  aks6d1c2  42747  sticksstones2  42764  sticksstones3  42765  qsalrel  42857  prjcrvfval  43213  mzpmfp  43328  eldiophb  43338  diophrw  43340  tfsconcatrn  43919  rp-tfslim  43930  conrel1d  44239  iunrelexp0  44278  rntrclfv  44308  clsneibex  44678  neicvgbex  44688  rnsnf  45762  fsneqrn  45787  limsupval3  46266  limsupresre  46270  limsupresico  46274  limsuppnfdlem  46275  limsupvaluz  46282  limsupvaluzmpt  46291  limsupvaluz2  46312  supcnvlimsup  46314  supcnvlimsupmpt  46315  liminfval  46333  liminfval5  46339  limsupresxr  46340  liminfresxr  46341  liminfresico  46345  liminfvalxr  46357  fourierdlem60  46740  fourierdlem61  46741  sge0val  46940  sge0z  46949  sge0revalmpt  46952  sge0tsms  46954  sge0sup  46965  sge0split  46983  sge0fodjrnlem  46990  sge0seq  47020  meadjiunlem  47039  meaiuninclem  47054  omeiunle  47091  ovolval2lem  47217  ovolval4lem2  47224  ovolval5lem2  47227  ovolval5lem3  47228  ovolval5  47229  ovnovollem2  47231  smfsuplem2  47386  smfsup  47388  smfsupmpt  47389  smfinf  47392  smfinfmpt  47393  smflimsuplem1  47394  smflimsuplem2  47395  smflimsuplem4  47397  smflimsuplem5  47398  smflimsuplem7  47400  smflimsup  47402  fnrnafv  47756  afv2eq12d  47809  isubgredgss  48487  isubgredg  48488  stgredg  48578  gpgedg  48667  dmrnxp  49458  imaidfu  49731  idfudiag1lem  50144