MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rneqd Structured version   Visualization version   GIF version

Theorem rneqd 5385
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
StepHypRef Expression
1 rneqd.1 . 2 (𝜑𝐴 = 𝐵)
2 rneq 5383 . 2 (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
31, 2syl 17 1 (𝜑 → ran 𝐴 = ran 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  ran crn 5144
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-cnv 5151  df-dm 5153  df-rn 5154
This theorem is referenced by:  resima2  5467  resima2OLD  5468  imaeq1  5496  imaeq2  5497  resiima  5515  rnxpid  5602  xpima  5611  funimacnv  6008  fnima  6048  elxp4  7152  elxp5  7153  2ndval  7213  fo2nd  7231  f2ndres  7235  curry1  7314  curry2  7317  oarec  7687  en1  8064  xpassen  8095  xpdom2  8096  sbthlem4  8114  fodomr  8152  dffi3  8378  marypha2lem4  8385  ordtypelem9  8472  dfac12lem1  9003  dfac12r  9006  fin23lem32  9204  fin23lem34  9206  fin23lem35  9207  fin23lem36  9208  fin23lem38  9209  fin23lem39  9210  fin23lem41  9212  itunitc  9281  ttukeylem3  9371  fpwwe2lem6  9495  fpwwe2lem9  9498  wunex2  9598  wuncval2  9607  gruima  9662  rpnnen1lem6  11857  rpnnen1OLD  11863  hashf1lem1  13277  s1rn  13415  relexprng  13830  relexpfld  13833  limsupval  14249  vdwapfval  15722  vdwapval  15724  vdwmc  15729  vdwpc  15731  vdwlem6  15737  vdwlem8  15739  restval  16134  restid2  16138  prdsval  16162  prdsdsval  16185  prdsdsval2  16191  prdsdsval3  16192  imasval  16218  imasdsval  16222  isfull  16617  arwval  16740  gsumvalx  17317  conjsubg  17739  pmtrfrn  17924  psgnfval  17966  sylow1lem2  18060  sylow1lem4  18062  sylow1  18064  sylow2blem1  18081  sylow2b  18084  sylow3lem1  18088  sylow3lem2  18089  sylow3lem3  18090  sylow3lem5  18092  sylow3lem6  18093  sylow3  18094  lsmfval  18099  lsmvalx  18100  oppglsm  18103  subglsm  18132  lsmpropd  18136  efgval2  18183  efgi2  18184  efgtlen  18185  efgsdm  18189  efgsdmi  18191  efgsrel  18193  efgs1b  18195  efgsp1  18196  efgsres  18197  efgsfo  18198  efgrelexlemb  18209  frgpnabllem1  18322  iscyg  18327  iscyggen  18328  gsumxp  18421  dprdval  18448  ablfac2  18534  evlseu  19564  zncyg  19945  cygznlem2a  19964  frlmsplit2  20160  tgrest  21011  ordtval  21041  ordtbas2  21043  ordtcnv  21053  ordtrest  21054  ordtrest2  21056  ispnrm  21191  cmpfi  21259  txval  21415  xkoval  21438  ptval2  21452  ptpjopn  21463  xkoccn  21470  xkoptsub  21505  xkopt  21506  fmval  21794  fmf  21796  txflf  21857  cnextf  21917  subgntr  21957  opnsubg  21958  clsnsg  21960  snclseqg  21966  tsmsval2  21980  tsmsxplem1  22003  ustuqtoplem  22090  utopsnneiplem  22098  utopsnneip  22099  fmucndlem  22142  ressprdsds  22223  mopnval  22290  metuval  22401  metdsval  22697  lebnumlem1  22807  lebnumlem3  22809  pi1xfrcnvlem  22902  pi1xfrcnv  22903  minveclem3b  23245  elovolmr  23290  ovolctb  23304  ovoliunlem3  23318  ovolshftlem1  23323  voliunlem3  23366  voliun  23368  volsup  23370  uniioombllem2  23397  uniioombllem3  23399  mbflimsup  23478  itg1climres  23526  itg2monolem1  23562  itg2i1fseq  23567  itg2cnlem1  23573  ellimc2  23686  dvivth  23818  dvne0  23819  lhop2  23823  lhop  23824  mdegfval  23867  dchrptlem2  25035  dchrpt  25037  tglnunirn  25488  tgisline  25567  perpln1  25650  perpln2  25651  isperp  25652  ishpg  25696  lmif  25722  islmib  25724  edgval  25986  edgvalOLD  25987  edgopval  25989  edgstruct  25991  edgiedgbOLD  25993  edg0iedg0OLD  25995  uhgr2edg  26145  usgr1e  26182  cplgrop  26389  cusgrexi  26395  structtocusgr  26398  1loopgredg  26453  1egrvtxdg0  26463  umgr2v2eedg  26476  ex-ima  27429  bafval  27587  pj3i  29195  elimampt  29566  ofrn2  29570  ffsrn  29632  smatrcl  29990  ordtprsval  30092  ordtprsuni  30093  ordtcnvNEW  30094  ordtrestNEW  30095  ordtrest2NEW  30097  qqhval  30146  qqhval2  30154  prodindf  30213  esumval  30236  esumsnf  30254  esumrnmpt2  30258  esumfsupre  30261  esumsup  30279  sxval  30381  omsval  30483  omsfval  30484  carsggect  30508  sibf0  30524  sitgfval  30531  cvmlift3lem6  31432  mvtval  31523  mvrsval  31528  mrsubrn  31536  mrsub0  31539  mrsubf  31540  mrsubccat  31541  mrsubcn  31542  mrsubco  31544  mrsubvrs  31545  elmsubrn  31551  msubrn  31552  msubf  31555  mstaval  31567  msubvrs  31583  mclsval  31586  trpredeq1  31844  trpredeq2  31845  trpredeq3  31846  filnetlem4  32501  mptsnunlem  33315  dissneqlem  33317  poimirlem3  33542  poimirlem9  33548  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem24  33563  poimirlem30  33569  poimirlem32  33571  mblfinlem2  33577  ovoliunnfl  33581  voliunnfl  33583  isrngo  33826  drngoi  33880  rngohomval  33893  rngoisoval  33906  idlval  33942  pridlval  33962  maxidlval  33968  igenval  33990  symrelim  34445  lsatset  34595  docaffvalN  36727  docafvalN  36728  mzpmfp  37627  eldiophb  37637  diophrw  37639  conrel1d  38272  iunrelexp0  38311  rntrclfv  38341  clsneibex  38717  neicvgbex  38727  rnsnf  39684  fsneqrn  39717  mptima2  39771  limsupval3  40242  limsupresre  40246  limsupresico  40250  limsuppnfdlem  40251  limsupvaluz  40258  limsupvaluzmpt  40267  limsupvaluz2  40288  supcnvlimsup  40290  supcnvlimsupmpt  40291  liminfval  40309  liminfval5  40315  limsupresxr  40316  liminfresxr  40317  liminfresico  40321  liminfvalxr  40333  fourierdlem60  40701  fourierdlem61  40702  sge0val  40901  sge0z  40910  sge0revalmpt  40913  sge0tsms  40915  sge0sup  40926  sge0split  40944  sge0fodjrnlem  40951  sge0seq  40981  meadjiunlem  41000  meaiuninclem  41015  omeiunle  41052  ovolval2lem  41178  ovolval4lem2  41185  ovolval5lem2  41188  ovolval5lem3  41189  ovolval5  41190  ovnovollem2  41192  smfsuplem2  41339  smfsup  41341  smfsupmpt  41342  smfinf  41345  smfinfmpt  41346  smflimsuplem1  41347  smflimsuplem2  41348  smflimsuplem4  41350  smflimsuplem5  41351  smflimsuplem7  41353  smflimsup  41355  fnrnafv  41563
  Copyright terms: Public domain W3C validator