Theorem rneqd 5895

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

Syntax hints:   → wi 4   = wceq 1542  ran crn 5633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-cnv 5640  df-dm 5642  df-rn 5643

This theorem is referenced by:  resima2  5983  elimampt  6010  imaeq1  6022  imaeq2  6023  mptimass  6040  resiima  6043  imadifssran  6117  rnxpid  6139  xpima  6148  funimacnv  6581  fnima  6630  focofo  6767  rnfvprc  6836  elimampo  7505  elxp4  7874  elxp5  7875  2ndval  7946  fo2nd  7964  f2ndres  7968  curry1  8056  curry2  8059  oarec  8499  en1  8973  xpassen  9011  xpdom2  9012  sbthlem4  9030  fodomr  9068  fodomfir  9240  dffi3  9346  marypha2lem4  9353  ordtypelem9  9443  dfac12lem1  10066  dfac12r  10069  fin23lem32  10266  fin23lem34  10268  fin23lem35  10269  fin23lem36  10270  fin23lem38  10271  fin23lem39  10272  fin23lem41  10274  itunitc  10343  ttukeylem3  10433  fpwwe2lem5  10558  fpwwe2lem8  10561  wunex2  10661  wuncval2  10670  gruima  10725  rpnnen1lem6  12907  hashf1lem1  14390  s1rn  14535  s2rn  14898  s3rn  14899  s7rn  14900  relexprng  14981  relexprnd  14983  relexpfld  14984  limsupval  15409  vdwapfval  16911  vdwapval  16913  vdwmc  16918  vdwpc  16920  vdwlem6  16926  vdwlem8  16928  restval  17358  restid2  17362  prdsval  17387  prdsdsval  17410  prdsdsval2  17416  prdsdsval3  17417  imasval  17444  imasdsval  17448  isfull  17848  arwval  17979  gsumvalx  18613  conjsubg  19191  psgnfval  19441  sylow1lem2  19540  sylow1lem4  19542  sylow1  19544  sylow2blem1  19561  sylow2b  19564  sylow3lem1  19568  sylow3lem2  19569  sylow3lem3  19570  sylow3lem5  19572  sylow3lem6  19573  sylow3  19574  lsmfval  19579  lsmvalx  19580  oppglsm  19583  subglsm  19614  lsmpropd  19618  efgval2  19665  efgi2  19666  efgtlen  19667  efgsdm  19671  efgsdmi  19673  efgsrel  19675  efgs1b  19677  efgsp1  19678  efgsres  19679  efgsfo  19680  efgrelexlemb  19691  frgpnabllem1  19814  iscyg  19820  iscyggen  19821  gsumxp  19917  dprdval  19946  ablfac2  20032  zncyg  21515  cygznlem2a  21534  frlmsplit2  21740  evlseu  22050  tgrest  23115  ordtval  23145  ordtbas2  23147  ordtcnv  23157  ordtrest  23158  ordtrest2  23160  ispnrm  23295  cmpfi  23364  txval  23520  xkoval  23543  ptval2  23557  ptpjopn  23568  xkoccn  23575  xkoptsub  23610  xkopt  23611  fmval  23899  fmf  23901  txflf  23962  cnextf  24022  subgntr  24063  opnsubg  24064  clsnsg  24066  snclseqg  24072  tsmsval2  24086  tsmsxplem1  24109  ustuqtoplem  24195  utopsnneiplem  24203  utopsnneip  24204  fmucndlem  24246  ressprdsds  24327  mopnval  24394  metuval  24505  metdsval  24804  lebnumlem1  24928  lebnumlem3  24930  pi1xfrcnvlem  25024  pi1xfrcnv  25025  minveclem3b  25396  elovolmr  25445  ovolctb  25459  ovoliunlem3  25473  ovolshftlem1  25478  voliunlem3  25521  voliun  25523  volsup  25525  uniioombllem2  25552  uniioombllem3  25554  mbflimsup  25635  itg1climres  25683  itg2monolem1  25719  itg2i1fseq  25724  itg2cnlem1  25730  ellimc2  25846  dvivth  25983  dvne0  25984  lhop2  25988  lhop  25989  mdegfval  26035  dchrptlem2  27244  dchrpt  27246  seqsval  28296  om2noseqfo  28306  tglnunirn  28632  tgisline  28711  perpln1  28794  perpln2  28795  isperp  28796  ishpg  28843  lmif  28869  islmib  28871  edgval  29134  edgopval  29136  edgstruct  29138  uhgr2edg  29293  usgr1e  29330  cplgrop  29522  cusgrexi  29528  structtocusgr  29531  1loopgredg  29587  1egrvtxdg0  29597  umgr2v2eedg  29610  ex-ima  30529  bafval  30692  pj3i  32296  ofrn2  32730  rnressnsn  32767  ffsrn  32818  prodindf  32955  pfxrn2  33033  pfxrn3  33034  swrdrn2  33047  swrdrn3  33048  gsumzresunsn  33156  gsumhashmul  33161  tocycfv  33203  tocycf  33211  trsp2cyc  33217  cycpmco2f1  33218  cycpmco2rn  33219  cycpmconjvlem  33235  cycpmconjslem2  33249  domnprodeq0  33370  qusbas2  33499  qusima  33501  qusrn  33502  nsgmgc  33505  nsgqusf1olem2  33507  idlsrgval  33596  esplyfval1  33750  esplyfvaln  33751  esplyind  33752  algextdeglem4  33898  smatrcl  33974  ordtprsval  34096  ordtprsuni  34097  ordtcnvNEW  34098  ordtrestNEW  34099  ordtrest2NEW  34101  qqhval  34150  qqhval2  34160  esumval  34224  esumsnf  34242  esumrnmpt2  34246  esumfsupre  34249  esumsup  34267  sxval  34368  omsval  34471  omsfval  34472  carsggect  34496  sibf0  34512  sitgfval  34519  cvmlift3lem6  35540  satfrnmapom  35586  mvtval  35716  mvrsval  35721  mrsubvrs  35738  elmsubrn  35744  msubrn  35745  mstaval  35760  msubvrs  35776  mclsval  35779  filnetlem4  36597  mptsnunlem  37593  dissneqlem  37595  exrecfnlem  37634  ctbssinf  37661  poimirlem3  37874  poimirlem9  37880  poimirlem16  37887  poimirlem17  37888  poimirlem19  37890  poimirlem20  37891  poimirlem24  37895  poimirlem30  37901  poimirlem32  37903  mblfinlem2  37909  ovoliunnfl  37913  voliunnfl  37915  isrngo  38148  drngoi  38202  rngohomval  38215  rngoisoval  38228  idlval  38264  pridlval  38284  maxidlval  38290  igenval  38312  cnvref4  38601  symrelim  38894  unidmqs  38990  lsatset  39366  docaffvalN  41497  docafvalN  41498  aks6d1c2  42500  sticksstones2  42517  sticksstones3  42518  qsalrel  42611  prjcrvfval  42989  mzpmfp  43104  eldiophb  43114  diophrw  43116  tfsconcatrn  43699  rp-tfslim  43710  conrel1d  44019  iunrelexp0  44058  rntrclfv  44088  clsneibex  44458  neicvgbex  44468  rnsnf  45543  fsneqrn  45569  limsupval3  46050  limsupresre  46054  limsupresico  46058  limsuppnfdlem  46059  limsupvaluz  46066  limsupvaluzmpt  46075  limsupvaluz2  46096  supcnvlimsup  46098  supcnvlimsupmpt  46099  liminfval  46117  liminfval5  46123  limsupresxr  46124  liminfresxr  46125  liminfresico  46129  liminfvalxr  46141  fourierdlem60  46524  fourierdlem61  46525  sge0val  46724  sge0z  46733  sge0revalmpt  46736  sge0tsms  46738  sge0sup  46749  sge0split  46767  sge0fodjrnlem  46774  sge0seq  46804  meadjiunlem  46823  meaiuninclem  46838  omeiunle  46875  ovolval2lem  47001  ovolval4lem2  47008  ovolval5lem2  47011  ovolval5lem3  47012  ovolval5  47013  ovnovollem2  47015  smfsuplem2  47170  smfsup  47172  smfsupmpt  47173  smfinf  47176  smfinfmpt  47177  smflimsuplem1  47178  smflimsuplem2  47179  smflimsuplem4  47181  smflimsuplem5  47182  smflimsuplem7  47184  smflimsup  47186  fnrnafv  47522  afv2eq12d  47575  isubgredgss  48225  isubgredg  48226  stgredg  48316  gpgedg  48405  dmrnxp  49196  imaidfu  49469  idfudiag1lem  49882