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

Theorem rneqd 5503
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 5501 . 2 (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
31, 2syl 17 1 (𝜑 → ran 𝐴 = ran 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1634  ran crn 5264
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-rab 3073  df-v 3357  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-nul 4074  df-if 4236  df-sn 4327  df-pr 4329  df-op 4333  df-br 4798  df-opab 4860  df-cnv 5271  df-dm 5273  df-rn 5274
This theorem is referenced by:  resima2  5584  imaeq1  5612  imaeq2  5613  resiima  5631  rnxpid  5719  xpima  5728  funimacnv  6121  fnima  6161  rnfvprc  6342  elxp4  7278  elxp5  7279  2ndval  7339  fo2nd  7357  f2ndres  7361  curry1  7441  curry2  7444  oarec  7817  en1  8197  xpassen  8231  xpdom2  8232  sbthlem4  8250  fodomr  8288  dffi3  8514  marypha2lem4  8521  ordtypelem9  8608  dfac12lem1  9188  dfac12r  9191  fin23lem32  9389  fin23lem34  9391  fin23lem35  9392  fin23lem36  9393  fin23lem38  9394  fin23lem39  9395  fin23lem41  9397  itunitc  9466  ttukeylem3  9556  fpwwe2lem6  9680  fpwwe2lem9  9683  wunex2  9783  wuncval2  9792  gruima  9847  rpnnen1lem6  12044  hashf1lem1  13463  s1rn  13601  relexprng  14016  relexpfld  14019  limsupval  14435  vdwapfval  15902  vdwapval  15904  vdwmc  15909  vdwpc  15911  vdwlem6  15917  vdwlem8  15919  restval  16315  restid2  16319  prdsval  16343  prdsdsval  16366  prdsdsval2  16372  prdsdsval3  16373  imasval  16399  imasdsval  16403  isfull  16797  arwval  16920  gsumvalx  17498  conjsubg  17920  psgnfval  18147  sylow1lem2  18241  sylow1lem4  18243  sylow1  18245  sylow2blem1  18262  sylow2b  18265  sylow3lem1  18269  sylow3lem2  18270  sylow3lem3  18271  sylow3lem5  18273  sylow3lem6  18274  sylow3  18275  lsmfval  18280  lsmvalx  18281  oppglsm  18284  subglsm  18313  lsmpropd  18317  efgval2  18364  efgi2  18365  efgtlen  18366  efgsdm  18370  efgsdmi  18372  efgsrel  18374  efgs1b  18376  efgsp1  18377  efgsres  18378  efgsfo  18379  efgrelexlemb  18390  frgpnabllem1  18503  iscyg  18508  iscyggen  18509  gsumxp  18602  dprdval  18630  ablfac2  18716  evlseu  19751  zncyg  20132  cygznlem2a  20151  frlmsplit2  20349  tgrest  21204  ordtval  21234  ordtbas2  21236  ordtcnv  21246  ordtrest  21247  ordtrest2  21249  ispnrm  21384  cmpfi  21452  txval  21608  xkoval  21631  ptval2  21645  ptpjopn  21656  xkoccn  21663  xkoptsub  21698  xkopt  21699  fmval  21987  fmf  21989  txflf  22050  cnextf  22110  subgntr  22150  opnsubg  22151  clsnsg  22153  snclseqg  22159  tsmsval2  22173  tsmsxplem1  22196  ustuqtoplem  22283  utopsnneiplem  22291  utopsnneip  22292  fmucndlem  22335  ressprdsds  22416  mopnval  22483  metuval  22594  metdsval  22890  lebnumlem1  23000  lebnumlem3  23002  pi1xfrcnvlem  23095  pi1xfrcnv  23096  minveclem3b  23438  elovolmr  23484  ovolctb  23498  ovoliunlem3  23512  ovolshftlem1  23517  voliunlem3  23560  voliun  23562  volsup  23564  uniioombllem2  23591  uniioombllem3  23593  mbflimsup  23674  itg1climres  23722  itg2monolem1  23758  itg2i1fseq  23763  itg2cnlem1  23769  ellimc2  23882  dvivth  24014  dvne0  24015  lhop2  24019  lhop  24020  mdegfval  24063  dchrptlem2  25232  dchrpt  25234  tglnunirn  25685  tgisline  25764  perpln1  25847  perpln2  25848  isperp  25849  ishpg  25893  lmif  25919  islmib  25921  edgval  26183  edgvalOLD  26184  edgopval  26186  edgstruct  26188  edgiedgbOLD  26190  edg0iedg0OLD  26192  uhgr2edg  26343  usgr1e  26381  cplgrop  26589  cusgrexi  26595  structtocusgr  26598  1loopgredg  26653  1egrvtxdg0  26663  umgr2v2eedg  26676  ex-ima  27658  bafval  27816  pj3i  29424  elimampt  29795  ofrn2  29799  ffsrn  29861  smatrcl  30219  ordtprsval  30321  ordtprsuni  30322  ordtcnvNEW  30323  ordtrestNEW  30324  ordtrest2NEW  30326  qqhval  30375  qqhval2  30383  prodindf  30442  esumval  30465  esumsnf  30483  esumrnmpt2  30487  esumfsupre  30490  esumsup  30508  sxval  30610  omsval  30712  omsfval  30713  carsggect  30737  sibf0  30753  sitgfval  30760  cvmlift3lem6  31661  mvtval  31752  mvrsval  31757  mrsubvrs  31774  elmsubrn  31780  msubrn  31781  mstaval  31796  msubvrs  31812  mclsval  31815  trpredeq1  32073  trpredeq2  32074  trpredeq3  32075  filnetlem4  32730  mptsnunlem  33539  dissneqlem  33541  poimirlem3  33762  poimirlem9  33768  poimirlem16  33775  poimirlem17  33776  poimirlem19  33778  poimirlem20  33779  poimirlem24  33783  poimirlem30  33789  poimirlem32  33791  mblfinlem2  33797  ovoliunnfl  33801  voliunnfl  33803  isrngo  34044  drngoi  34098  rngohomval  34111  rngoisoval  34124  idlval  34160  pridlval  34180  maxidlval  34186  igenval  34208  symrelim  34662  lsatset  34814  docaffvalN  36946  docafvalN  36947  mzpmfp  37851  eldiophb  37861  diophrw  37863  conrel1d  38495  iunrelexp0  38534  rntrclfv  38564  clsneibex  38940  neicvgbex  38950  rnsnf  39901  fsneqrn  39932  mptima2  39984  limsupval3  40448  limsupresre  40452  limsupresico  40456  limsuppnfdlem  40457  limsupvaluz  40464  limsupvaluzmpt  40473  limsupvaluz2  40494  supcnvlimsup  40496  supcnvlimsupmpt  40497  liminfval  40515  liminfval5  40521  limsupresxr  40522  liminfresxr  40523  liminfresico  40527  liminfvalxr  40539  fourierdlem60  40906  fourierdlem61  40907  sge0val  41106  sge0z  41115  sge0revalmpt  41118  sge0tsms  41120  sge0sup  41131  sge0split  41149  sge0fodjrnlem  41156  sge0seq  41186  meadjiunlem  41205  meaiuninclem  41220  omeiunle  41257  ovolval2lem  41383  ovolval4lem2  41390  ovolval5lem2  41393  ovolval5lem3  41394  ovolval5  41395  ovnovollem2  41397  smfsuplem2  41544  smfsup  41546  smfsupmpt  41547  smfinf  41550  smfinfmpt  41551  smflimsuplem1  41552  smflimsuplem2  41553  smflimsuplem4  41555  smflimsuplem5  41556  smflimsuplem7  41558  smflimsup  41560  fnrnafv  41787
  Copyright terms: Public domain W3C validator