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

Theorem eqeltrd 2216
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 2208 . 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 1331    e. wcel 1480
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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135
This theorem is referenced by:  eqeltrrd  2217  3eltr4d  2223  eqeltrid  2226  eqeltrdi  2230  ifcldadc  3501  ifcldcd  3507  intab  3800  disjiun  3924  iinexgm  4079  opexg  4150  tfisi  4501  nnpredcl  4536  imain  5205  fvmptd  5502  fvmptdf  5508  fvmptt  5512  elfvmptrab  5516  dffo3  5567  resfunexg  5641  f1oiso2  5728  riota2df  5750  riota5f  5754  ovmpodxf  5896  ovmpodf  5902  offval  5989  ofvalg  5991  offeq  5995  iunexg  6017  oprabexd  6025  fo1stresm  6059  fo2ndresm  6060  oprssdmm  6069  1stdm  6080  1stconst  6118  2ndconst  6119  cnvf1olem  6121  fo2ndf  6124  f1od2  6132  iunon  6181  tfrlemibacc  6223  tfrlemibfn  6225  tfr1onlembacc  6239  tfr1onlembfn  6241  tfrcllembacc  6252  tfrcllembfn  6254  tfrcl  6261  rdgon  6283  frec0g  6294  freccllem  6299  frecfcllem  6301  frecsuclem  6303  oacl  6356  omcl  6357  oeicl  6358  nntr2  6399  mptelixpg  6628  fidifsnen  6764  en2eqpr  6801  unfiin  6814  ssfirab  6822  fnfi  6825  relcnvfi  6829  fidcenumlemr  6843  elfi2  6860  supclti  6885  supubti  6886  suplubti  6887  supelti  6889  ordiso2  6920  djulclr  6934  djurclr  6935  djulcl  6936  djurcl  6937  djuss  6955  updjudhcoinlf  6965  updjudhcoinrg  6966  ctssdclemn0  6995  ctssdccl  6996  ctssdc  6998  enumctlemm  6999  cardcl  7037  cc2lem  7081  cc3  7083  addclpi  7142  mulclpi  7143  addclnq  7190  mulclnq  7191  addclnq0  7266  mulclnq0  7267  nqpnq0nq  7268  elnp1st2nd  7291  prarloclemcalc  7317  distrlem1prl  7397  distrlem1pru  7398  ltexprlemopl  7416  ltexprlemopu  7418  ltexprlemfl  7424  ltexprlemrl  7425  ltexprlemfu  7426  ltexprlemru  7427  addcanprlemu  7430  recexprlemloc  7446  aptiprleml  7454  caucvgprprlemopl  7512  suplocexprlemex  7537  addclsr  7568  mulclsr  7569  recexgt0sr  7588  mulextsr1lem  7595  suplocsrlemb  7621  suplocsrlempr  7622  suplocsrlem  7623  axaddcl  7679  axaddrcl  7680  axmulcl  7681  axmulrcl  7682  axcaucvglemval  7712  subcl  7968  cru  8371  aprcl  8415  divclap  8445  redivclap  8498  diveqap1bd  8602  lbinfcl  8714  cju  8726  nn1m1nn  8745  nnsub  8766  nnnn0addcl  9014  un0addcl  9017  peano2z  9097  peano2zm  9099  zaddcllemneg  9100  zaddcl  9101  nnaddm1cl  9122  nn0n0n1ge2  9128  zdivadd  9147  zdivmul  9148  suprzclex  9156  zneo  9159  peano5uzti  9166  supinfneg  9397  infsupneg  9398  qmulz  9422  qnegcl  9435  qapne  9438  qdivcl  9442  cnref1o  9447  xnegcl  9622  xltnegi  9625  xaddnemnf  9647  xaddnepnf  9648  xnegdi  9658  xnpcan  9662  xltadd1  9666  xposdif  9672  xleaddadd  9677  iccf1o  9794  ige3m2fz  9836  ige2m1fz1  9896  rebtwn2z  10039  flqcl  10053  flapcl  10055  ceilqcl  10088  intfracq  10100  modqcl  10106  mulqmod0  10110  modqdifz  10116  zmodcl  10124  modfzo0difsn  10175  modsumfzodifsn  10176  frec2uzzd  10180  frec2uzsucd  10181  frec2uzuzd  10182  frecuzrdgrrn  10188  frec2uzrdg  10189  frecuzrdgrcl  10190  frecuzrdgsuc  10194  frecuzrdgrclt  10195  frecuzrdgg  10196  frecuzrdgsuctlem  10203  fzofig  10212  iseqovex  10236  seq3val  10238  seqvalcd  10239  seqf  10241  seqovcd  10243  seq3clss  10247  seq3caopr3  10261  iseqf1olemnab  10268  iseqf1olemqk  10274  iseqf1olemjpcl  10275  iseqf1olemqpcl  10276  iseqf1olemfvp  10277  seq3f1olemqsumkj  10278  seq3f1olemqsum  10280  seq3f1oleml  10283  seq3f1o  10284  seq3distr  10293  ser0f  10295  ser3le  10298  exp3vallem  10301  exp3val  10302  exp1  10306  expcl2lemap  10312  m1expcl2  10322  expaddzap  10344  sqcl  10361  nnsqcl  10369  qsqcl  10371  zesq  10417  facp1  10483  faccl  10488  facdiv  10491  bcval  10502  bcrpcl  10506  bcp1n  10514  bcpasc  10519  permnn  10524  hashennn  10533  hashcl  10534  shftlem  10595  ovshftex  10598  shftf  10609  seq3shft  10617  cjth  10625  imval  10629  recl  10632  imcl  10633  crre  10636  remim  10639  reim0b  10641  cvg1nlemcau  10763  uzin2  10766  resqrexlem1arp  10784  resqrexlemp1rp  10785  resqrexlemglsq  10801  resqrexlemga  10802  resqrtcl  10808  abscl  10830  absrpclap  10840  nn0abscl  10864  fzomaxdiflem  10891  fzomaxdif  10892  maxabslemab  10985  maxcl  10989  zmaxcl  11003  minmax  11008  mincl  11009  xrmaxcl  11028  xrmaxaddlem  11036  xrminmax  11041  xrmincl  11042  xrmineqinf  11045  xrminrpcl  11050  reccn2ap  11089  climaddc1  11105  climmulc2  11107  climsubc1  11108  climsubc2  11109  climle  11110  climlec2  11117  climcvg1nlem  11125  sumrbdclem  11153  fsum3cvg  11154  summodclem3  11156  summodclem2a  11157  zsumdc  11160  fsumgcl  11162  fsum3  11163  isumss  11167  fisumss  11168  isumss2  11169  fsum3cvg2  11170  fsum3ser  11173  fsumcl2lem  11174  fsumcllem  11175  fsumadd  11182  sumsnf  11185  fsumsplitsn  11186  isumcl  11201  isummulc2  11202  isumrecl  11205  isumge0  11206  isumadd  11207  fsum2dlemstep  11210  fisumcom2  11214  mptfzshft  11218  fsumrev  11219  fsummulc2  11224  iserabs  11251  isumshft  11266  isumsplit  11267  isum1p  11268  isumrpcl  11270  isumle  11271  isumlessdc  11272  trireciplem  11276  expcnvap0  11278  expcnvre  11279  expcnv  11280  explecnv  11281  geolim  11287  geolim2  11288  geo2lim  11292  cvgratnnlemsumlt  11304  cvgratz  11308  mertenslemub  11310  mertenslemi1  11311  mertenslem2  11312  mertensabs  11313  prodf1f  11319  prodfdivap  11323  prodrbdclem  11347  fproddccvg  11348  prodmodclem3  11351  prodmodclem2a  11352  efcllemp  11371  ef0lem  11373  efcvgfsum  11380  reefcl  11381  ege2le3  11384  efcj  11386  efaddlem  11387  eftlcvg  11400  eftlcl  11401  reeftlcl  11402  eftlub  11403  efsep  11404  effsumlt  11405  efgt1p2  11408  efgt1p  11409  reeff1  11413  tanclap  11422  resincl  11433  recoscl  11434  retanclap  11435  eirraplem  11489  dvdsval2  11502  sqoddm1div8z  11589  zssinfcl  11647  infssuzex  11648  infssuzcldc  11650  gcdval  11654  gcdn0cl  11657  gcddvds  11658  divgcdnnr  11670  nn0seqcvgd  11728  ialgrlem1st  11729  ialgrlemconst  11730  algrf  11732  algrp1  11733  eucalgf  11742  eucalglt  11744  lcmval  11750  lcmcllem  11754  lcmgcdlem  11764  cncongr2  11791  sqrt2irrlem  11845  oddpwdclemxy  11853  oddpwdclemdc  11857  qden1elz  11889  phicl2  11896  phimullem  11907  ennnfonelemjn  11921  ennnfonelemg  11922  ennnfonelemp1  11925  ctinfomlemom  11946  ctiunctlemfo  11958  setsex  12000  strsetsid  12001  ressid2  12027  ressval2  12028  ressid  12029  iunopn  12178  toponmax  12201  tgvalex  12228  tgtop  12246  tgiun  12251  tgidm  12252  ntropn  12295  tgrest  12347  restopnb  12359  cnovex  12374  cnclima  12401  txvalex  12432  txtop  12438  tx1cn  12447  tx2cn  12448  txcnp  12449  txcnmpt  12451  txdis1cn  12456  cnmptcom  12476  imasnopn  12477  hmeocnv  12485  hmeores  12493  txhmeo  12497  txswaphmeo  12499  ispsmet  12501  xmetres  12560  metres  12561  blex  12565  xmeter  12614  xmetresbl  12618  mopntopon  12621  isxms2  12630  xmetxp  12685  xmettx  12688  txmetcnp  12696  qtopbasss  12699  qtopbas  12700  reopnap  12716  ioo2blex  12722  blssioo  12723  tgioo  12724  fsumcncntop  12734  cncfval  12737  divccncfap  12755  cdivcncfap  12765  ivthdec  12800  limccnpcntop  12822  dvrecap  12855  pilem3  12880  tanrpcl  12934  cosordlem  12946  ioocosf1o  12951  djucllem  13060  nninfsellemeq  13263  qdencn  13275  isomninnlem  13278  cvgcmp2nlemabs  13280  trilpolemclim  13282  trilpolemisumle  13284  trilpolemeq1  13286  trilpolemlt1  13287
  Copyright terms: Public domain W3C validator