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

Theorem rneqd 5554
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 5552 . 2 (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
31, 2syl 17 1 (𝜑 → ran 𝐴 = ran 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  ran crn 5312
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-br 4845  df-opab 4907  df-cnv 5319  df-dm 5321  df-rn 5322
This theorem is referenced by:  resima2  5635  imaeq1  5671  imaeq2  5672  resiima  5690  rnxpid  5778  xpima  5787  funimacnv  6177  fnima  6217  rnfvprc  6398  elxp4  7336  elxp5  7337  2ndval  7397  fo2nd  7415  f2ndres  7419  curry1  7499  curry2  7502  oarec  7875  en1  8255  xpassen  8289  xpdom2  8290  sbthlem4  8308  fodomr  8346  dffi3  8572  marypha2lem4  8579  ordtypelem9  8666  dfac12lem1  9246  dfac12r  9249  fin23lem32  9447  fin23lem34  9449  fin23lem35  9450  fin23lem36  9451  fin23lem38  9452  fin23lem39  9453  fin23lem41  9455  itunitc  9524  ttukeylem3  9614  fpwwe2lem6  9738  fpwwe2lem9  9741  wunex2  9841  wuncval2  9850  gruima  9905  rpnnen1lem6  12034  hashf1lem1  13452  s1rn  13590  relexprng  14005  relexpfld  14008  limsupval  14424  vdwapfval  15888  vdwapval  15890  vdwmc  15895  vdwpc  15897  vdwlem6  15903  vdwlem8  15905  restval  16288  restid2  16292  prdsval  16316  prdsdsval  16339  prdsdsval2  16345  prdsdsval3  16346  imasval  16372  imasdsval  16376  isfull  16770  arwval  16893  gsumvalx  17471  conjsubg  17890  psgnfval  18117  sylow1lem2  18211  sylow1lem4  18213  sylow1  18215  sylow2blem1  18232  sylow2b  18235  sylow3lem1  18239  sylow3lem2  18240  sylow3lem3  18241  sylow3lem5  18243  sylow3lem6  18244  sylow3  18245  lsmfval  18250  lsmvalx  18251  oppglsm  18254  subglsm  18283  lsmpropd  18287  efgval2  18334  efgi2  18335  efgtlen  18336  efgsdm  18340  efgsdmi  18342  efgsrel  18344  efgs1b  18346  efgsp1  18347  efgsres  18348  efgsfo  18349  efgrelexlemb  18360  frgpnabllem1  18473  iscyg  18478  iscyggen  18479  gsumxp  18572  dprdval  18600  ablfac2  18686  evlseu  19720  zncyg  20100  cygznlem2a  20119  frlmsplit2  20318  tgrest  21173  ordtval  21203  ordtbas2  21205  ordtcnv  21215  ordtrest  21216  ordtrest2  21218  ispnrm  21353  cmpfi  21421  txval  21577  xkoval  21600  ptval2  21614  ptpjopn  21625  xkoccn  21632  xkoptsub  21667  xkopt  21668  fmval  21956  fmf  21958  txflf  22019  cnextf  22079  subgntr  22119  opnsubg  22120  clsnsg  22122  snclseqg  22128  tsmsval2  22142  tsmsxplem1  22165  ustuqtoplem  22252  utopsnneiplem  22260  utopsnneip  22261  fmucndlem  22304  ressprdsds  22385  mopnval  22452  metuval  22563  metdsval  22859  lebnumlem1  22969  lebnumlem3  22971  pi1xfrcnvlem  23064  pi1xfrcnv  23065  minveclem3b  23407  elovolmr  23453  ovolctb  23467  ovoliunlem3  23481  ovolshftlem1  23486  voliunlem3  23529  voliun  23531  volsup  23533  uniioombllem2  23560  uniioombllem3  23562  mbflimsup  23643  itg1climres  23691  itg2monolem1  23727  itg2i1fseq  23732  itg2cnlem1  23738  ellimc2  23851  dvivth  23983  dvne0  23984  lhop2  23988  lhop  23989  mdegfval  24032  dchrptlem2  25200  dchrpt  25202  tglnunirn  25653  tgisline  25732  perpln1  25815  perpln2  25816  isperp  25817  ishpg  25861  lmif  25887  islmib  25889  edgval  26151  edgvalOLD  26152  edgopval  26154  edgstruct  26156  edgiedgbOLD  26158  edg0iedg0OLD  26160  uhgr2edg  26311  usgr1e  26349  cplgrop  26557  cusgrexi  26563  structtocusgr  26566  1loopgredg  26621  1egrvtxdg0  26631  umgr2v2eedg  26644  ex-ima  27626  bafval  27783  pj3i  29391  elimampt  29761  ofrn2  29765  ffsrn  29827  smatrcl  30183  ordtprsval  30285  ordtprsuni  30286  ordtcnvNEW  30287  ordtrestNEW  30288  ordtrest2NEW  30290  qqhval  30339  qqhval2  30347  prodindf  30406  esumval  30429  esumsnf  30447  esumrnmpt2  30451  esumfsupre  30454  esumsup  30472  sxval  30574  omsval  30676  omsfval  30677  carsggect  30701  sibf0  30717  sitgfval  30724  cvmlift3lem6  31624  mvtval  31715  mvrsval  31720  mrsubvrs  31737  elmsubrn  31743  msubrn  31744  mstaval  31759  msubvrs  31775  mclsval  31778  trpredeq1  32035  trpredeq2  32036  trpredeq3  32037  filnetlem4  32692  mptsnunlem  33497  dissneqlem  33499  poimirlem3  33720  poimirlem9  33726  poimirlem16  33733  poimirlem17  33734  poimirlem19  33736  poimirlem20  33737  poimirlem24  33741  poimirlem30  33747  poimirlem32  33749  mblfinlem2  33755  ovoliunnfl  33759  voliunnfl  33761  isrngo  34002  drngoi  34056  rngohomval  34069  rngoisoval  34082  idlval  34118  pridlval  34138  maxidlval  34144  igenval  34166  symrelim  34613  lsatset  34765  docaffvalN  36896  docafvalN  36897  mzpmfp  37806  eldiophb  37816  diophrw  37818  conrel1d  38449  iunrelexp0  38488  rntrclfv  38518  clsneibex  38894  neicvgbex  38904  rnsnf  39853  fsneqrn  39884  mptima2  39935  limsupval3  40398  limsupresre  40402  limsupresico  40406  limsuppnfdlem  40407  limsupvaluz  40414  limsupvaluzmpt  40423  limsupvaluz2  40444  supcnvlimsup  40446  supcnvlimsupmpt  40447  liminfval  40465  liminfval5  40471  limsupresxr  40472  liminfresxr  40473  liminfresico  40477  liminfvalxr  40489  fourierdlem60  40856  fourierdlem61  40857  sge0val  41056  sge0z  41065  sge0revalmpt  41068  sge0tsms  41070  sge0sup  41081  sge0split  41099  sge0fodjrnlem  41106  sge0seq  41136  meadjiunlem  41155  meaiuninclem  41170  omeiunle  41207  ovolval2lem  41333  ovolval4lem2  41340  ovolval5lem2  41343  ovolval5lem3  41344  ovolval5  41345  ovnovollem2  41347  smfsuplem2  41494  smfsup  41496  smfsupmpt  41497  smfinf  41500  smfinfmpt  41501  smflimsuplem1  41502  smflimsuplem2  41503  smflimsuplem4  41505  smflimsuplem5  41506  smflimsuplem7  41508  smflimsup  41510  fnrnafv  41745  afv2eq12d  41798
  Copyright terms: Public domain W3C validator