MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eleqtrri Unicode version

Theorem eleqtrri 2356
Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eleqtrr.1  |-  A  e.  B
eleqtrr.2  |-  C  =  B
Assertion
Ref Expression
eleqtrri  |-  A  e.  C

Proof of Theorem eleqtrri
StepHypRef Expression
1 eleqtrr.1 . 2  |-  A  e.  B
2 eleqtrr.2 . . 3  |-  C  =  B
32eqcomi 2287 . 2  |-  B  =  C
41, 3eleqtri 2355 1  |-  A  e.  C
Colors of variables: wff set class
Syntax hints:    = wceq 1623    e. wcel 1684
This theorem is referenced by:  3eltr4i  2362  opi1  4240  opi2  4241  seqomlem3  6464  oneo  6579  nnneo  6649  0elixp  6847  ac6sfi  7101  oancom  7352  tz9.13  7463  rankval  7488  rankid  7505  ssrankr1  7507  rankel  7511  rankval3  7512  rankpw  7515  rankss  7521  ranksn  7526  rankuni2  7527  rankun  7528  rankpr  7529  rankop  7530  rankeq0  7533  rankr1b  7536  fin1a2lem4  8029  fin1a2lem6  8031  hsmexlem6  8057  dcomex  8073  axdc3lem4  8079  canthp1lem2  8275  pwxpndom2  8287  rankcf  8399  grutsk  8444  axgroth3  8453  inaprc  8458  1lt2pi  8529  1nn  9757  pnfxr  10455  mnfxr  10456  uzrdg0i  11022  axdc4uzlem  11044  eqs1  11447  infcvgaux1i  12315  0bits  12630  sadcf  12644  prmreclem6  12968  xpsfrnel2  13467  setcepi  13920  grpss  14503  efgi0  15029  efgi1  15030  vrgpf  15077  vrgpinv  15078  frgpuptinv  15080  frgpup2  15085  frgpnabllem1  15161  dmdprdpr  15284  dprdpr  15285  leordtval2  16942  xpstopnlem1  17500  xpstopnlem2  17502  ptcmp  17752  tsmsfbas  17810  zcld  18319  abscncfALT  18423  iimulcn  18436  icopnfhmeo  18441  iccpnfhmeo  18443  xrhmeo  18444  dveflem  19326  ftc1  19389  efopnlem2  20004  cxpcn3  20088  efrlim  20264  hhshsslem2  21845  nonbooli  22230  nmopadjlei  22668  xrge0iifhmeo  23318  lmxrge0  23375  dya2iocbrsiga  23578  coinflippvt  23685  subfacp1lem2a  23711  subfacp1lem5  23715  erdszelem5  23726  erdszelem8  23729  konigsberg  23911  sinccvglem  24005  wfrlem14  24269  wfrlem16  24271  rankeq1o  24801  0hf  24807  onint1  24888  dominc  25280  rninc  25281  cinei  25623  1ded  25738  empklst  26009  pgapspf  26052  fdc  26455  reheibor  26563  pw2f1ocnv  27130  psgnunilem2  27418  rfcnpre1  27690  usgraex0elv  28128  usgraex1elv  28129  usgraex2elv  28130  usgraex3elv  28131  sucidALTVD  28646  sucidALT  28647  sucidVD  28648  bnj97  28898  bnj553  28930  bnj966  28976  bnj1442  29079
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-cleq 2276  df-clel 2279
  Copyright terms: Public domain W3C validator