Theorem rneqd 5808

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

Syntax hints:   → wi 4   = wceq 1537  ran crn 5556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-cnv 5563  df-dm 5565  df-rn 5566

This theorem is referenced by:  resima2  5888  imaeq1  5924  imaeq2  5925  resiima  5944  rnxpid  6030  xpima  6039  funimacnv  6435  fnima  6478  rnfvprc  6664  elxp4  7627  elxp5  7628  2ndval  7692  fo2nd  7710  f2ndres  7714  curry1  7799  curry2  7802  oarec  8188  en1  8576  xpassen  8611  xpdom2  8612  sbthlem4  8630  fodomr  8668  dffi3  8895  marypha2lem4  8902  ordtypelem9  8990  dfac12lem1  9569  dfac12r  9572  fin23lem32  9766  fin23lem34  9768  fin23lem35  9769  fin23lem36  9770  fin23lem38  9771  fin23lem39  9772  fin23lem41  9774  itunitc  9843  ttukeylem3  9933  fpwwe2lem6  10057  fpwwe2lem9  10060  wunex2  10160  wuncval2  10169  gruima  10224  rpnnen1lem6  12382  hashf1lem1  13814  s1rn  13953  relexprng  14405  relexpfld  14408  limsupval  14831  vdwapfval  16307  vdwapval  16309  vdwmc  16314  vdwpc  16316  vdwlem6  16322  vdwlem8  16324  restval  16700  restid2  16704  prdsval  16728  prdsdsval  16751  prdsdsval2  16757  prdsdsval3  16758  imasval  16784  imasdsval  16788  isfull  17180  arwval  17303  gsumvalx  17886  conjsubg  18390  psgnfval  18628  sylow1lem2  18724  sylow1lem4  18726  sylow1  18728  sylow2blem1  18745  sylow2b  18748  sylow3lem1  18752  sylow3lem2  18753  sylow3lem3  18754  sylow3lem5  18756  sylow3lem6  18757  sylow3  18758  lsmfval  18763  lsmvalx  18764  oppglsm  18767  subglsm  18799  lsmpropd  18803  efgval2  18850  efgi2  18851  efgtlen  18852  efgsdm  18856  efgsdmi  18858  efgsrel  18860  efgs1b  18862  efgsp1  18863  efgsres  18864  efgsfo  18865  efgrelexlemb  18876  frgpnabllem1  18993  iscyg  18998  iscyggen  18999  gsumxp  19096  dprdval  19125  ablfac2  19211  rnrhmsubrg  19567  evlseu  20296  zncyg  20695  cygznlem2a  20714  frlmsplit2  20917  tgrest  21767  ordtval  21797  ordtbas2  21799  ordtcnv  21809  ordtrest  21810  ordtrest2  21812  ispnrm  21947  cmpfi  22016  txval  22172  xkoval  22195  ptval2  22209  ptpjopn  22220  xkoccn  22227  xkoptsub  22262  xkopt  22263  fmval  22551  fmf  22553  txflf  22614  cnextf  22674  subgntr  22715  opnsubg  22716  clsnsg  22718  snclseqg  22724  tsmsval2  22738  tsmsxplem1  22761  ustuqtoplem  22848  utopsnneiplem  22856  utopsnneip  22857  fmucndlem  22900  ressprdsds  22981  mopnval  23048  metuval  23159  metdsval  23455  lebnumlem1  23565  lebnumlem3  23567  pi1xfrcnvlem  23660  pi1xfrcnv  23661  minveclem3b  24031  elovolmr  24077  ovolctb  24091  ovoliunlem3  24105  ovolshftlem1  24110  voliunlem3  24153  voliun  24155  volsup  24157  uniioombllem2  24184  uniioombllem3  24186  mbflimsup  24267  itg1climres  24315  itg2monolem1  24351  itg2i1fseq  24356  itg2cnlem1  24362  ellimc2  24475  dvivth  24607  dvne0  24608  lhop2  24612  lhop  24613  mdegfval  24656  dchrptlem2  25841  dchrpt  25843  tglnunirn  26334  tgisline  26413  perpln1  26496  perpln2  26497  isperp  26498  ishpg  26545  lmif  26571  islmib  26573  edgval  26834  edgopval  26836  edgstruct  26838  uhgr2edg  26990  usgr1e  27027  cplgrop  27219  cusgrexi  27225  structtocusgr  27228  1loopgredg  27283  1egrvtxdg0  27293  umgr2v2eedg  27306  ex-ima  28221  bafval  28381  pj3i  29985  elimampt  30383  ofrn2  30387  ffsrn  30465  pfxrn2  30616  pfxrn3  30617  swrdrn2  30628  swrdrn3  30629  gsumzresunsn  30691  tocycfv  30751  tocycf  30759  trsp2cyc  30765  cycpmco2f1  30766  cycpmco2rn  30767  cycpmconjvlem  30783  cycpmconjslem2  30797  smatrcl  31061  ordtprsval  31161  ordtprsuni  31162  ordtcnvNEW  31163  ordtrestNEW  31164  ordtrest2NEW  31166  qqhval  31215  qqhval2  31223  prodindf  31282  esumval  31305  esumsnf  31323  esumrnmpt2  31327  esumfsupre  31330  esumsup  31348  sxval  31449  omsval  31551  omsfval  31552  carsggect  31576  sibf0  31592  sitgfval  31599  cvmlift3lem6  32571  satfrnmapom  32617  mvtval  32747  mvrsval  32752  mrsubvrs  32769  elmsubrn  32775  msubrn  32776  mstaval  32791  msubvrs  32807  mclsval  32810  trpredeq1  33059  trpredeq2  33060  trpredeq3  33061  filnetlem4  33729  mptsnunlem  34622  dissneqlem  34624  exrecfnlem  34663  ctbssinf  34690  poimirlem3  34910  poimirlem9  34916  poimirlem16  34923  poimirlem17  34924  poimirlem19  34926  poimirlem20  34927  poimirlem24  34931  poimirlem30  34937  poimirlem32  34939  mblfinlem2  34945  ovoliunnfl  34949  voliunnfl  34951  isrngo  35190  drngoi  35244  rngohomval  35257  rngoisoval  35270  idlval  35306  pridlval  35326  maxidlval  35332  igenval  35354  symrelim  35810  unidmqs  35903  lsatset  36141  docaffvalN  38272  docafvalN  38273  qsalrel  39174  mzpmfp  39393  eldiophb  39403  diophrw  39405  conrel1d  40057  iunrelexp0  40096  rntrclfv  40126  clsneibex  40501  neicvgbex  40511  rnsnf  41493  fsneqrn  41523  mptima2  41566  limsupval3  42022  limsupresre  42026  limsupresico  42030  limsuppnfdlem  42031  limsupvaluz  42038  limsupvaluzmpt  42047  limsupvaluz2  42068  supcnvlimsup  42070  supcnvlimsupmpt  42071  liminfval  42089  liminfval5  42095  limsupresxr  42096  liminfresxr  42097  liminfresico  42101  liminfvalxr  42113  fourierdlem60  42500  fourierdlem61  42501  sge0val  42697  sge0z  42706  sge0revalmpt  42709  sge0tsms  42711  sge0sup  42722  sge0split  42740  sge0fodjrnlem  42747  sge0seq  42777  meadjiunlem  42796  meaiuninclem  42811  omeiunle  42848  ovolval2lem  42974  ovolval4lem2  42981  ovolval5lem2  42984  ovolval5lem3  42985  ovolval5  42986  ovnovollem2  42988  smfsuplem2  43135  smfsup  43137  smfsupmpt  43138  smfinf  43141  smfinfmpt  43142  smflimsuplem1  43143  smflimsuplem2  43144  smflimsuplem4  43146  smflimsuplem5  43147  smflimsuplem7  43149  smflimsup  43151  fnrnafv  43410  afv2eq12d  43463