Theorem rneqd 5932

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ran crn 5659

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-cnv 5666  df-dm 5668  df-rn 5669

This theorem is used by:  elimampt  6053  imaeq1  6065  imaeq2  6066  resima2  6075  mptimass  6089  resiima  6092  rnxpid  6183  xpima  6192  imadifssranOLDOLD  6222  funimacnv  6651  fnima  6699  focofo  6839  rnfvprc  6910  elimampo  7589  elxp4  7968  elxp5  7969  2ndval  8038  fo2nd  8056  f2ndres  8060  curry1  8152  curry2  8155  oarec  8608  en1  9089  xpassen  9128  xpdom2  9129  sbthlem4  9147  fodomr  9185  fodomfir  9357  dffi3  9460  marypha2lem4  9467  ordtypelem9  9557  dfac12lem1  10261  dfac12r  10264  fin23lem32  10461  fin23lem34  10463  fin23lem35  10464  fin23lem36  10465  fin23lem38  10466  fin23lem39  10467  fin23lem41  10469  itunitc  10538  ttukeylem3  10628  fpwwe2lem5  10759  fpwwe2lem8  10762  wunex2  10862  wuncval2  10871  gruima  10926  rpnnen1lem6  13150  hashf1lem1  14641  s1rn  14787  swrdrn3  14844  s2rn  15159  s3rn  15160  s7rn  15161  relexprng  15242  relexprnd  15244  relexpfld  15245  limsupval  15685  vdwapfval  17193  vdwapval  17195  vdwmc  17200  vdwpc  17202  vdwlem6  17208  vdwlem8  17210  restval  17647  restid2  17651  prdsval  17676  prdsdsval  17699  prdsdsval2  17705  prdsdsval3  17706  imasval  17733  imasdsval  17737  isfull  18137  arwval  18268  gsumvalx  18915  conjsubg  19514  psgnfval  19765  sylow1lem2  19864  sylow1lem4  19866  sylow1  19868  sylow2blem1  19885  sylow2b  19888  sylow3lem1  19892  sylow3lem2  19893  sylow3lem3  19894  sylow3lem5  19896  sylow3lem6  19897  sylow3  19898  lsmfval  19903  lsmvalx  19904  oppglsm  19907  subglsm  19938  lsmpropd  19942  efgval2  19989  efgi2  19990  efgtlen  19991  efgsdm  19995  efgsdmi  19997  efgsrel  19999  efgs1b  20001  efgsp1  20002  efgsres  20003  efgsfo  20004  efgrelexlemb  20015  frgpnabllem1  20138  iscyg  20144  iscyggen  20145  gsumxp  20241  dprdval  20270  ablfac2  20356  zncyg  21909  cygznlem2a  21928  frlmsplit2  22134  evlseu  22447  tgrest  23532  ordtval  23562  ordtbas2  23564  ordtcnv  23574  ordtrest  23575  ordtrest2  23577  ispnrm  23712  cmpfi  23781  txval  23938  xkoval  23961  ptval2  23975  ptpjopn  23986  xkoccn  23993  xkoptsub  24028  xkopt  24029  fmval  24317  fmf  24319  txflf  24380  cnextf  24440  subgntr  24481  opnsubg  24482  clsnsg  24484  snclseqg  24490  tsmsval2  24504  tsmsxplem1  24527  ustuqtoplem  24613  utopsnneiplem  24621  utopsnneip  24622  fmucndlem  24664  ressprdsds  24745  mopnval  24812  metuval  24923  metdsval  25222  lebnumlem1  25337  lebnumlem3  25339  pi1xfrcnvlem  25432  pi1xfrcnv  25433  minveclem3b  25804  elovolmr  25852  ovolctb  25866  ovoliunlem3  25880  ovolshftlem1  25885  voliunlem3  25928  voliun  25930  volsup  25932  uniioombllem2  25959  uniioombllem3  25961  mbflimsup  26042  itg1climres  26090  itg2monolem1  26126  itg2i1fseq  26131  itg2cnlem1  26137  ellimc2  26252  dvivth  26385  dvne0  26386  lhop2  26390  lhop  26391  mdegfval  26435  dchrptlem2  27649  dchrpt  27651  seqsval  28731  om2noseqfo  28741  tglnunirn  29068  tgisline  29152  perpln1  29242  perpln2  29243  isperp  29244  ishpg  29294  tgplnfn  29310  plngval  29312  isplng  29313  lmif  29347  islmib  29349  cgrabasimass  29435  brprlng  29473  edgval  29684  edgopval  29686  edgstruct  29688  uhgr2edg  29846  usgr1e  29883  cplgrop  30075  cusgrexi  30081  structtocusgr  30084  1loopgredg  30139  1egrvtxdg0  30149  umgr2v2eedg  30162  ex-ima  31100  bafval  31263  pj3i  32867  ofrn2  33332  rnressnsn  33368  ffsrn  33416  prodindf  33525  pfxrn2  33603  pfxrn3  33604  swrdrn2  33613  gsumzresunsn  33722  gsumhashmul  33727  tocycfv  33769  tocycf  33777  trsp2cyc  33783  cycpmco2f1  33784  cycpmco2rn  33785  cycpmconjvlem  33801  cycpmconjslem2  33815  domnprodeq0  33939  qusbas2  34061  qusima  34063  qusrn  34064  nsgmgc  34067  nsgqusf1olem2  34069  idlsrgval  34139  esplyfval1  34316  esplyfvaln  34317  esplyind  34318  algextdeglem4  34463  smatrcl  34539  ordtprsval  34661  ordtprsuni  34662  ordtcnvNEW  34663  ordtrestNEW  34664  ordtrest2NEW  34666  qqhval  34715  qqhval2  34725  esumval  34789  esumsnf  34807  esumrnmpt2  34811  esumfsupre  34814  esumsup  34832  sxval  34934  omsval  35036  omsfval  35037  carsggect  35061  sibf0  35077  sitgfval  35084  cvmlift3lem6  36297  satfrnmapom  36343  mvtval  36473  mvrsval  36478  mrsubvrs  36495  elmsubrn  36501  msubrn  36502  mstaval  36517  msubvrs  36533  mclsval  36536  filnetlem4  37384  mptsnunlem  38529  dissneqlem  38531  exrecfnlem  38570  ctbssinf  38597  poimirlem3  38809  poimirlem9  38815  poimirlem16  38822  poimirlem17  38823  poimirlem19  38825  poimirlem20  38826  poimirlem24  38830  poimirlem30  38836  poimirlem32  38838  mblfinlem2  38844  ovoliunnfl  38848  voliunnfl  38850  isrngo  39097  drngoi  39151  rngohomval  39164  rngoisoval  39177  idlval  39213  pridlval  39233  maxidlval  39239  igenval  39261  cnvref4  39548  symrelim  39841  unidmqs  39937  lsatset  40313  docaffvalN  42444  docafvalN  42445  aks6d1c2  43446  sticksstones2  43463  sticksstones3  43464  qsalrel  43559  prjcrvfval  43933  mzpmfp  44024  eldiophb  44034  diophrw  44036  tfsconcatrn  44605  rp-tfslim  44616  conrel1d  44924  iunrelexp0  44963  rntrclfv  44993  clsneibex  45363  neicvgbex  45373  rnsnf  46472  fsneqrn  46497  limsupval3  46975  limsupresre  46979  limsupresico  46983  limsuppnfdlem  46984  limsupvaluz  46991  limsupvaluzmpt  47000  limsupvaluz2  47021  supcnvlimsup  47023  supcnvlimsupmpt  47024  liminfval  47042  liminfval5  47048  limsupresxr  47049  liminfresxr  47050  liminfresico  47054  liminfvalxr  47066  fourierdlem60  47449  fourierdlem61  47450  sge0val  47649  sge0z  47658  sge0revalmpt  47661  sge0tsms  47663  sge0sup  47674  sge0split  47692  sge0fodjrnlem  47699  sge0seq  47729  meadjiunlem  47748  meaiuninclem  47763  omeiunle  47800  ovolval2lem  47926  ovolval4lem2  47933  ovolval5lem2  47936  ovolval5lem3  47937  ovolval5  47938  ovnovollem2  47940  smfsuplem2  48095  smfsup  48097  smfsupmpt  48098  smfinf  48101  smfinfmpt  48102  smflimsuplem1  48103  smflimsuplem2  48104  smflimsuplem4  48106  smflimsuplem5  48107  smflimsuplem7  48109  smflimsup  48111  tmachlem-uassst  48226  fnrnafv  48505  afv2eq12d  48558  isubgredgss  49236  isubgredg  49237  stgredg  49327  gpgedg  49416  dmrnxp  50279  imaidfu  50557  idfudiag1lem  50989