Theorem rneqd 5353

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

Syntax hints:   → wi 4   = wceq 1483  ran crn 5115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-cnv 5122  df-dm 5124  df-rn 5125

This theorem is referenced by:  resima2  5432  resima2OLD  5433  imaeq1  5461  imaeq2  5462  resiima  5480  rnxpid  5567  xpima  5576  funimacnv  5970  fnima  6010  elxp4  7110  elxp5  7111  2ndval  7171  fo2nd  7189  f2ndres  7191  curry1  7269  curry2  7272  oarec  7642  en1  8023  xpassen  8054  xpdom2  8055  sbthlem4  8073  fodomr  8111  dffi3  8337  marypha2lem4  8344  ordtypelem9  8431  dfac12lem1  8965  dfac12r  8968  fin23lem32  9166  fin23lem34  9168  fin23lem35  9169  fin23lem36  9170  fin23lem38  9171  fin23lem39  9172  fin23lem41  9174  itunitc  9243  ttukeylem3  9333  fpwwe2lem6  9457  fpwwe2lem9  9460  wunex2  9560  wuncval2  9569  gruima  9624  rpnnen1lem6  11819  rpnnen1OLD  11825  hashf1lem1  13239  s1rn  13379  relexprng  13786  relexpfld  13789  limsupval  14205  vdwapfval  15675  vdwapval  15677  vdwmc  15682  vdwpc  15684  vdwlem6  15690  vdwlem8  15692  restval  16087  restid2  16091  prdsval  16115  prdsdsval  16138  prdsdsval2  16144  prdsdsval3  16145  imasval  16171  imasdsval  16175  isfull  16570  arwval  16693  gsumvalx  17270  conjsubg  17692  pmtrfrn  17878  psgnfval  17920  sylow1lem2  18014  sylow1lem4  18016  sylow1  18018  sylow2blem1  18035  sylow2b  18038  sylow3lem1  18042  sylow3lem2  18043  sylow3lem3  18044  sylow3lem5  18046  sylow3lem6  18047  sylow3  18048  lsmfval  18053  lsmvalx  18054  oppglsm  18057  subglsm  18086  lsmpropd  18090  efgval2  18137  efgi2  18138  efgtlen  18139  efgsdm  18143  efgsdmi  18145  efgsrel  18147  efgs1b  18149  efgsp1  18150  efgsres  18151  efgsfo  18152  efgrelexlemb  18163  frgpnabllem1  18276  iscyg  18281  iscyggen  18282  gsumxp  18375  dprdval  18402  ablfac2  18488  evlseu  19516  zncyg  19897  cygznlem2a  19916  frlmsplit2  20112  tgrest  20963  ordtval  20993  ordtbas2  20995  ordtcnv  21005  ordtrest  21006  ordtrest2  21008  ispnrm  21143  cmpfi  21211  txval  21367  xkoval  21390  ptval2  21404  ptpjopn  21415  xkoccn  21422  xkoptsub  21457  xkopt  21458  fmval  21747  fmf  21749  txflf  21810  cnextf  21870  subgntr  21910  opnsubg  21911  clsnsg  21913  snclseqg  21919  tsmsval2  21933  tsmsxplem1  21956  ustuqtoplem  22043  utopsnneiplem  22051  utopsnneip  22052  fmucndlem  22095  ressprdsds  22176  mopnval  22243  metuval  22354  metdsval  22650  lebnumlem1  22760  lebnumlem3  22762  pi1xfrcnvlem  22856  pi1xfrcnv  22857  minveclem3b  23199  elovolmr  23244  ovolctb  23258  ovoliunlem3  23272  ovolshftlem1  23277  voliunlem3  23320  voliun  23322  volsup  23324  uniioombllem2  23351  uniioombllem3  23353  mbflimsup  23433  itg1climres  23481  itg2monolem1  23517  itg2i1fseq  23522  itg2cnlem1  23528  ellimc2  23641  dvivth  23773  dvne0  23774  lhop2  23778  lhop  23779  mdegfval  23822  dchrptlem2  24990  dchrpt  24992  tglnunirn  25443  tgisline  25522  perpln1  25605  perpln2  25606  isperp  25607  ishpg  25651  lmif  25677  islmib  25679  edgval  25941  edgvalOLD  25942  edgopval  25944  edgstruct  25946  edgiedgbOLD  25948  edg0iedg0OLD  25950  uhgr2edg  26100  usgr1e  26137  cplgrop  26333  cusgrexi  26339  structtocusgr  26342  1loopgredg  26397  1egrvtxdg0  26407  umgr2v2eedg  26420  ex-ima  27299  bafval  27459  pj3i  29067  elimampt  29438  ofrn2  29442  ffsrn  29504  smatrcl  29862  ordtprsval  29964  ordtprsuni  29965  ordtcnvNEW  29966  ordtrestNEW  29967  ordtrest2NEW  29969  qqhval  30018  qqhval2  30026  prodindf  30085  esumval  30108  esumsnf  30126  esumrnmpt2  30130  esumfsupre  30133  esumsup  30151  sxval  30253  omsval  30355  omsfval  30356  carsggect  30380  sibf0  30396  sitgfval  30403  cvmlift3lem6  31306  mvtval  31397  mvrsval  31402  mrsubrn  31410  mrsub0  31413  mrsubf  31414  mrsubccat  31415  mrsubcn  31416  mrsubco  31418  mrsubvrs  31419  elmsubrn  31425  msubrn  31426  msubf  31429  mstaval  31441  msubvrs  31457  mclsval  31460  trpredeq1  31720  trpredeq2  31721  trpredeq3  31722  filnetlem4  32376  mptsnunlem  33185  dissneqlem  33187  poimirlem3  33412  poimirlem9  33418  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem24  33433  poimirlem30  33439  poimirlem32  33441  mblfinlem2  33447  ovoliunnfl  33451  voliunnfl  33453  isrngo  33696  drngoi  33750  rngohomval  33763  rngoisoval  33776  idlval  33812  pridlval  33832  maxidlval  33838  igenval  33860  lsatset  34277  docaffvalN  36410  docafvalN  36411  mzpmfp  37310  eldiophb  37320  diophrw  37322  conrel1d  37955  iunrelexp0  37994  rntrclfv  38024  clsneibex  38400  neicvgbex  38410  csbima12gALTOLD  39057  rnsnf  39370  fsneqrn  39403  mptima2  39457  limsupval3  39924  limsupresre  39928  limsupresico  39932  limsuppnfdlem  39933  limsupvaluz  39940  limsupvaluzmpt  39949  limsupvaluz2  39970  supcnvlimsup  39972  supcnvlimsupmpt  39973  liminfval  39991  liminfval5  39997  limsupresxr  39998  liminfresxr  39999  liminfresico  40003  liminfvalxr  40015  fourierdlem60  40383  fourierdlem61  40384  sge0val  40583  sge0z  40592  sge0revalmpt  40595  sge0tsms  40597  sge0sup  40608  sge0split  40626  sge0fodjrnlem  40633  sge0seq  40663  meadjiunlem  40682  meaiuninclem  40697  omeiunle  40731  ovolval2lem  40857  ovolval4lem2  40864  ovolval5lem2  40867  ovolval5lem3  40868  ovolval5  40869  ovnovollem2  40871  smfsuplem2  41018  smfsup  41020  smfsupmpt  41021  smfinf  41024  smfinfmpt  41025  smflimsuplem1  41026  smflimsuplem2  41027  smflimsuplem4  41029  smflimsuplem5  41030  smflimsuplem7  41032  smflimsup  41034  fnrnafv  41242