Theorem rneqd 5931

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

Syntax hints:   → wi 4   = wceq 1533  ran crn 5670

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-rab 3427  df-v 3470  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-br 5142  df-opab 5204  df-cnv 5677  df-dm 5679  df-rn 5680

This theorem is referenced by:  resima2  6010  imaeq1  6048  imaeq2  6049  mptimass  6066  resiima  6069  rnxpid  6166  xpima  6175  funimacnv  6623  fnima  6674  focofo  6812  rnfvprc  6879  elxp4  7912  elxp5  7913  2ndval  7977  fo2nd  7995  f2ndres  7999  curry1  8090  curry2  8093  oarec  8563  en1  9023  en1OLD  9024  xpassen  9068  xpdom2  9069  sbthlem4  9088  fodomr  9130  dffi3  9428  marypha2lem4  9435  ordtypelem9  9523  dfac12lem1  10140  dfac12r  10143  fin23lem32  10341  fin23lem34  10343  fin23lem35  10344  fin23lem36  10345  fin23lem38  10346  fin23lem39  10347  fin23lem41  10349  itunitc  10418  ttukeylem3  10508  fpwwe2lem5  10632  fpwwe2lem8  10635  wunex2  10735  wuncval2  10744  gruima  10799  rpnnen1lem6  12970  hashf1lem1  14421  hashf1lem1OLD  14422  s1rn  14555  relexprng  14999  relexprnd  15001  relexpfld  15002  limsupval  15424  vdwapfval  16913  vdwapval  16915  vdwmc  16920  vdwpc  16922  vdwlem6  16928  vdwlem8  16930  restval  17381  restid2  17385  prdsval  17410  prdsdsval  17433  prdsdsval2  17439  prdsdsval3  17440  imasval  17466  imasdsval  17470  isfull  17872  arwval  18005  gsumvalx  18609  conjsubg  19175  psgnfval  19420  sylow1lem2  19519  sylow1lem4  19521  sylow1  19523  sylow2blem1  19540  sylow2b  19543  sylow3lem1  19547  sylow3lem2  19548  sylow3lem3  19549  sylow3lem5  19551  sylow3lem6  19552  sylow3  19553  lsmfval  19558  lsmvalx  19559  oppglsm  19562  subglsm  19593  lsmpropd  19597  efgval2  19644  efgi2  19645  efgtlen  19646  efgsdm  19650  efgsdmi  19652  efgsrel  19654  efgs1b  19656  efgsp1  19657  efgsres  19658  efgsfo  19659  efgrelexlemb  19670  frgpnabllem1  19793  iscyg  19799  iscyggen  19800  gsumxp  19896  dprdval  19925  ablfac2  20011  rnrhmsubrg  20507  zncyg  21443  cygznlem2a  21462  frlmsplit2  21668  evlseu  21988  tgrest  23018  ordtval  23048  ordtbas2  23050  ordtcnv  23060  ordtrest  23061  ordtrest2  23063  ispnrm  23198  cmpfi  23267  txval  23423  xkoval  23446  ptval2  23460  ptpjopn  23471  xkoccn  23478  xkoptsub  23513  xkopt  23514  fmval  23802  fmf  23804  txflf  23865  cnextf  23925  subgntr  23966  opnsubg  23967  clsnsg  23969  snclseqg  23975  tsmsval2  23989  tsmsxplem1  24012  ustuqtoplem  24099  utopsnneiplem  24107  utopsnneip  24108  fmucndlem  24151  ressprdsds  24232  mopnval  24299  metuval  24413  metdsval  24718  lebnumlem1  24842  lebnumlem3  24844  pi1xfrcnvlem  24938  pi1xfrcnv  24939  minveclem3b  25311  elovolmr  25360  ovolctb  25374  ovoliunlem3  25388  ovolshftlem1  25393  voliunlem3  25436  voliun  25438  volsup  25440  uniioombllem2  25467  uniioombllem3  25469  mbflimsup  25550  itg1climres  25599  itg2monolem1  25635  itg2i1fseq  25640  itg2cnlem1  25646  ellimc2  25761  dvivth  25898  dvne0  25899  lhop2  25903  lhop  25904  mdegfval  25953  dchrptlem2  27153  dchrpt  27155  seqsval  28116  om2noseqfo  28126  tglnunirn  28307  tgisline  28386  perpln1  28469  perpln2  28470  isperp  28471  ishpg  28518  lmif  28544  islmib  28546  edgval  28817  edgopval  28819  edgstruct  28821  uhgr2edg  28973  usgr1e  29010  cplgrop  29202  cusgrexi  29208  structtocusgr  29211  1loopgredg  29267  1egrvtxdg0  29277  umgr2v2eedg  29290  ex-ima  30204  bafval  30366  pj3i  31970  elimampt  32371  ofrn2  32374  ffsrn  32461  pfxrn2  32611  pfxrn3  32612  swrdrn2  32623  swrdrn3  32624  gsumzresunsn  32712  gsumhashmul  32714  tocycfv  32774  tocycf  32782  trsp2cyc  32788  cycpmco2f1  32789  cycpmco2rn  32790  cycpmconjvlem  32806  cycpmconjslem2  32820  qusbas2  33023  qusima  33025  qusrn  33026  nsgmgc  33029  nsgqusf1olem2  33031  idlsrgval  33123  algextdeglem4  33297  smatrcl  33306  ordtprsval  33428  ordtprsuni  33429  ordtcnvNEW  33430  ordtrestNEW  33431  ordtrest2NEW  33433  qqhval  33484  qqhval2  33492  prodindf  33551  esumval  33574  esumsnf  33592  esumrnmpt2  33596  esumfsupre  33599  esumsup  33617  sxval  33718  omsval  33822  omsfval  33823  carsggect  33847  sibf0  33863  sitgfval  33870  cvmlift3lem6  34843  satfrnmapom  34889  mvtval  35019  mvrsval  35024  mrsubvrs  35041  elmsubrn  35047  msubrn  35048  mstaval  35063  msubvrs  35079  mclsval  35082  filnetlem4  35774  mptsnunlem  36726  dissneqlem  36728  exrecfnlem  36767  ctbssinf  36794  poimirlem3  37004  poimirlem9  37010  poimirlem16  37017  poimirlem17  37018  poimirlem19  37020  poimirlem20  37021  poimirlem24  37025  poimirlem30  37031  poimirlem32  37033  mblfinlem2  37039  ovoliunnfl  37043  voliunnfl  37045  isrngo  37278  drngoi  37332  rngohomval  37345  rngoisoval  37358  idlval  37394  pridlval  37414  maxidlval  37420  igenval  37442  cnvref4  37732  symrelim  37942  unidmqs  38037  lsatset  38373  docaffvalN  40505  docafvalN  40506  aks6d1c2  41507  sticksstones2  41525  sticksstones3  41526  qsalrel  41628  prjcrvfval  41956  mzpmfp  42068  eldiophb  42078  diophrw  42080  tfsconcatrn  42673  rp-tfslim  42684  conrel1d  42995  iunrelexp0  43034  rntrclfv  43064  clsneibex  43434  neicvgbex  43444  rnsnf  44460  fsneqrn  44487  limsupval3  44985  limsupresre  44989  limsupresico  44993  limsuppnfdlem  44994  limsupvaluz  45001  limsupvaluzmpt  45010  limsupvaluz2  45031  supcnvlimsup  45033  supcnvlimsupmpt  45034  liminfval  45052  liminfval5  45058  limsupresxr  45059  liminfresxr  45060  liminfresico  45064  liminfvalxr  45076  fourierdlem60  45459  fourierdlem61  45460  sge0val  45659  sge0z  45668  sge0revalmpt  45671  sge0tsms  45673  sge0sup  45684  sge0split  45702  sge0fodjrnlem  45709  sge0seq  45739  meadjiunlem  45758  meaiuninclem  45773  omeiunle  45810  ovolval2lem  45936  ovolval4lem2  45943  ovolval5lem2  45946  ovolval5lem3  45947  ovolval5  45948  ovnovollem2  45950  smfsuplem2  46105  smfsup  46107  smfsupmpt  46108  smfinf  46111  smfinfmpt  46112  smflimsuplem1  46113  smflimsuplem2  46114  smflimsuplem4  46116  smflimsuplem5  46117  smflimsuplem7  46119  smflimsup  46121  fnrnafv  46447  afv2eq12d  46500