ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqeltrd Unicode version

Theorem eqeltrd 2194
Description: Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.)
Hypotheses
Ref Expression
eqeltrd.1  |-  ( ph  ->  A  =  B )
eqeltrd.2  |-  ( ph  ->  B  e.  C )
Assertion
Ref Expression
eqeltrd  |-  ( ph  ->  A  e.  C )

Proof of Theorem eqeltrd
StepHypRef Expression
1 eqeltrd.2 . 2  |-  ( ph  ->  B  e.  C )
2 eqeltrd.1 . . 3  |-  ( ph  ->  A  =  B )
32eleq1d 2186 . 2  |-  ( ph  ->  ( A  e.  C  <->  B  e.  C ) )
41, 3mpbird 166 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1316    e. wcel 1465
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110  df-clel 2113
This theorem is referenced by:  eqeltrrd  2195  3eltr4d  2201  eqeltrid  2204  syl6eqel  2208  ifcldadc  3471  ifcldcd  3477  intab  3770  disjiun  3894  iinexgm  4049  opexg  4120  tfisi  4471  nnpredcl  4506  imain  5175  fvmptd  5470  fvmptdf  5476  fvmptt  5480  elfvmptrab  5484  dffo3  5535  resfunexg  5609  f1oiso2  5696  riota2df  5718  riota5f  5722  ovmpodxf  5864  ovmpodf  5870  offval  5957  ofvalg  5959  offeq  5963  iunexg  5985  oprabexd  5993  fo1stresm  6027  fo2ndresm  6028  oprssdmm  6037  1stdm  6048  1stconst  6086  2ndconst  6087  cnvf1olem  6089  fo2ndf  6092  f1od2  6100  iunon  6149  tfrlemibacc  6191  tfrlemibfn  6193  tfr1onlembacc  6207  tfr1onlembfn  6209  tfrcllembacc  6220  tfrcllembfn  6222  tfrcl  6229  rdgon  6251  frec0g  6262  freccllem  6267  frecfcllem  6269  frecsuclem  6271  oacl  6324  omcl  6325  oeicl  6326  nntr2  6367  mptelixpg  6596  fidifsnen  6732  en2eqpr  6769  unfiin  6782  ssfirab  6790  fnfi  6793  relcnvfi  6797  fidcenumlemr  6811  elfi2  6828  supclti  6853  supubti  6854  suplubti  6855  supelti  6857  ordiso2  6888  djulclr  6902  djurclr  6903  djulcl  6904  djurcl  6905  djuss  6923  updjudhcoinlf  6933  updjudhcoinrg  6934  ctssdclemn0  6963  ctssdccl  6964  ctssdc  6966  enumctlemm  6967  cardcl  7005  addclpi  7103  mulclpi  7104  addclnq  7151  mulclnq  7152  addclnq0  7227  mulclnq0  7228  nqpnq0nq  7229  elnp1st2nd  7252  prarloclemcalc  7278  distrlem1prl  7358  distrlem1pru  7359  ltexprlemopl  7377  ltexprlemopu  7379  ltexprlemfl  7385  ltexprlemrl  7386  ltexprlemfu  7387  ltexprlemru  7388  addcanprlemu  7391  recexprlemloc  7407  aptiprleml  7415  caucvgprprlemopl  7473  suplocexprlemex  7498  addclsr  7529  mulclsr  7530  recexgt0sr  7549  mulextsr1lem  7556  suplocsrlemb  7582  suplocsrlempr  7583  suplocsrlem  7584  axaddcl  7640  axaddrcl  7641  axmulcl  7642  axmulrcl  7643  axcaucvglemval  7673  subcl  7929  cru  8331  aprcl  8375  divclap  8405  redivclap  8458  diveqap1bd  8562  lbinfcl  8671  cju  8683  nn1m1nn  8702  nnsub  8723  nnnn0addcl  8965  un0addcl  8968  peano2z  9048  peano2zm  9050  zaddcllemneg  9051  zaddcl  9052  nnaddm1cl  9073  nn0n0n1ge2  9079  zdivadd  9098  zdivmul  9099  suprzclex  9107  zneo  9110  peano5uzti  9117  supinfneg  9346  infsupneg  9347  qmulz  9371  qnegcl  9384  qapne  9387  qdivcl  9391  cnref1o  9396  xnegcl  9570  xltnegi  9573  xaddnemnf  9595  xaddnepnf  9596  xnegdi  9606  xnpcan  9610  xltadd1  9614  xposdif  9620  xleaddadd  9625  iccf1o  9742  ige3m2fz  9784  ige2m1fz1  9844  rebtwn2z  9987  flqcl  10001  flapcl  10003  ceilqcl  10036  intfracq  10048  modqcl  10054  mulqmod0  10058  modqdifz  10064  zmodcl  10072  modfzo0difsn  10123  modsumfzodifsn  10124  frec2uzzd  10128  frec2uzsucd  10129  frec2uzuzd  10130  frecuzrdgrrn  10136  frec2uzrdg  10137  frecuzrdgrcl  10138  frecuzrdgsuc  10142  frecuzrdgrclt  10143  frecuzrdgg  10144  frecuzrdgsuctlem  10151  fzofig  10160  iseqovex  10184  seq3val  10186  seqvalcd  10187  seqf  10189  seqovcd  10191  seq3clss  10195  seq3caopr3  10209  iseqf1olemnab  10216  iseqf1olemqk  10222  iseqf1olemjpcl  10223  iseqf1olemqpcl  10224  iseqf1olemfvp  10225  seq3f1olemqsumkj  10226  seq3f1olemqsum  10228  seq3f1oleml  10231  seq3f1o  10232  seq3distr  10241  ser0f  10243  ser3le  10246  exp3vallem  10249  exp3val  10250  exp1  10254  expcl2lemap  10260  m1expcl2  10270  expaddzap  10292  sqcl  10309  nnsqcl  10317  qsqcl  10319  zesq  10365  facp1  10431  faccl  10436  facdiv  10439  bcval  10450  bcrpcl  10454  bcp1n  10462  bcpasc  10467  permnn  10472  hashennn  10481  hashcl  10482  shftlem  10543  ovshftex  10546  shftf  10557  seq3shft  10565  cjth  10573  imval  10577  recl  10580  imcl  10581  crre  10584  remim  10587  reim0b  10589  cvg1nlemcau  10711  uzin2  10714  resqrexlem1arp  10732  resqrexlemp1rp  10733  resqrexlemglsq  10749  resqrexlemga  10750  resqrtcl  10756  abscl  10778  absrpclap  10788  nn0abscl  10812  fzomaxdiflem  10839  fzomaxdif  10840  maxabslemab  10933  maxcl  10937  zmaxcl  10951  minmax  10956  mincl  10957  xrmaxcl  10976  xrmaxaddlem  10984  xrminmax  10989  xrmincl  10990  xrmineqinf  10993  xrminrpcl  10998  reccn2ap  11037  climaddc1  11053  climmulc2  11055  climsubc1  11056  climsubc2  11057  climle  11058  climlec2  11065  climcvg1nlem  11073  sumrbdclem  11100  fsum3cvg  11101  summodclem3  11104  summodclem2a  11105  zsumdc  11108  fsumgcl  11110  fsum3  11111  isumss  11115  fisumss  11116  isumss2  11117  fsum3cvg2  11118  fsum3ser  11121  fsumcl2lem  11122  fsumcllem  11123  fsumadd  11130  sumsnf  11133  fsumsplitsn  11134  isumcl  11149  isummulc2  11150  isumrecl  11153  isumge0  11154  isumadd  11155  fsum2dlemstep  11158  fisumcom2  11162  mptfzshft  11166  fsumrev  11167  fsummulc2  11172  iserabs  11199  isumshft  11214  isumsplit  11215  isum1p  11216  isumrpcl  11218  isumle  11219  isumlessdc  11220  trireciplem  11224  expcnvap0  11226  expcnvre  11227  expcnv  11228  explecnv  11229  geolim  11235  geolim2  11236  geo2lim  11240  cvgratnnlemsumlt  11252  cvgratz  11256  mertenslemub  11258  mertenslemi1  11259  mertenslem2  11260  mertensabs  11261  efcllemp  11278  ef0lem  11280  efcvgfsum  11287  reefcl  11288  ege2le3  11291  efcj  11293  efaddlem  11294  eftlcvg  11307  eftlcl  11308  reeftlcl  11309  eftlub  11310  efsep  11311  effsumlt  11312  efgt1p2  11315  efgt1p  11316  reeff1  11321  tanclap  11330  resincl  11341  recoscl  11342  retanclap  11343  eirraplem  11395  dvdsval2  11408  sqoddm1div8z  11495  zssinfcl  11553  infssuzex  11554  infssuzcldc  11556  gcdval  11560  gcdn0cl  11563  gcddvds  11564  divgcdnnr  11576  nn0seqcvgd  11634  ialgrlem1st  11635  ialgrlemconst  11636  algrf  11638  algrp1  11639  eucalgf  11648  eucalglt  11650  lcmval  11656  lcmcllem  11660  lcmgcdlem  11670  cncongr2  11697  sqrt2irrlem  11751  oddpwdclemxy  11758  oddpwdclemdc  11762  qden1elz  11794  phicl2  11801  phimullem  11812  ennnfonelemjn  11826  ennnfonelemg  11827  ennnfonelemp1  11830  ctinfomlemom  11851  ctiunctlemfo  11863  setsex  11902  strsetsid  11903  ressid2  11929  ressval2  11930  ressid  11931  iunopn  12080  toponmax  12103  tgvalex  12130  tgtop  12148  tgiun  12153  tgidm  12154  ntropn  12197  tgrest  12249  restopnb  12261  cnovex  12276  cnclima  12303  txvalex  12334  txtop  12340  tx1cn  12349  tx2cn  12350  txcnp  12351  txcnmpt  12353  txdis1cn  12358  cnmptcom  12378  imasnopn  12379  hmeocnv  12387  hmeores  12395  txhmeo  12399  txswaphmeo  12401  ispsmet  12403  xmetres  12462  metres  12463  blex  12467  xmeter  12516  xmetresbl  12520  mopntopon  12523  isxms2  12532  xmetxp  12587  xmettx  12590  txmetcnp  12598  qtopbasss  12601  qtopbas  12602  reopnap  12618  ioo2blex  12624  blssioo  12625  tgioo  12626  fsumcncntop  12636  cncfval  12639  divccncfap  12657  cdivcncfap  12667  ivthdec  12702  limccnpcntop  12724  dvrecap  12757  pilem3  12775  djucllem  12903  nninfsellemeq  13106  qdencn  13118  isomninnlem  13121  cvgcmp2nlemabs  13123  trilpolemclim  13125  trilpolemisumle  13127  trilpolemeq1  13129  trilpolemlt1  13130
  Copyright terms: Public domain W3C validator