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

Theorem eqeltrrd 2217
Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
Hypotheses
Ref Expression
eqeltrrd.1  |-  ( ph  ->  A  =  B )
eqeltrrd.2  |-  ( ph  ->  A  e.  C )
Assertion
Ref Expression
eqeltrrd  |-  ( ph  ->  B  e.  C )

Proof of Theorem eqeltrrd
StepHypRef Expression
1 eqeltrrd.1 . . 3  |-  ( ph  ->  A  =  B )
21eqcomd 2145 . 2  |-  ( ph  ->  B  =  A )
3 eqeltrrd.2 . 2  |-  ( ph  ->  A  e.  C )
42, 3eqeltrd 2216 1  |-  ( ph  ->  B  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:  3eltr3d  2222  exmid01  4121  pwntru  4122  xpexr2m  4980  funimaexg  5207  fvmptdv2  5510  ffvresb  5583  2ndrn  6081  1st2ndbr  6082  elopabi  6093  cnvf1olem  6121  dftpos4  6160  tfrlemibxssdm  6224  tfr1onlembxssdm  6240  tfrcllembxssdm  6253  nnmordi  6412  th3qlem1  6531  infiexmid  6771  onunsnss  6805  ssfirab  6822  ssfidc  6823  fnfi  6825  fidcenumlemr  6843  elfi2  6860  ordiso2  6920  djulclb  6940  ctmlemr  6993  ctssdccl  6996  ctssdc  6998  exmidfodomrlemreseldju  7063  exmidfodomrlemr  7065  archnqq  7239  prarloclemarch2  7241  enq0tr  7256  nqnq0  7263  addcmpblnq0  7265  mulcmpblnq0  7266  mulcanenq0ec  7267  addclnq0  7273  mulclnq0  7274  nqpnq0nq  7275  nq0m0r  7278  distrnq0  7281  addassnq0lemcl  7283  prarloclemlt  7315  prarloclem5  7322  distrlem4prl  7406  distrlem4pru  7407  ltexprlemm  7422  ltexprlemrl  7432  ltexprlemru  7434  addcanprleml  7436  cauappcvgprlemladdru  7478  prsrlem1  7564  mulgt0sr  7600  axpre-suploclemres  7723  cnegexlem2  7952  subf  7978  resubcl  8040  negcon1ad  8082  subeq0bd  8155  rimul  8361  rereim  8362  aprcl  8422  nn0nnaddcl  9022  elnn0nn  9033  zaddcllemneg  9107  zsubcl  9109  zrevaddcl  9118  elz2  9136  zdiv  9153  peano5uzti  9173  peano2uzr  9394  uzaddcl  9395  divfnzn  9427  qsubcl  9444  qrevaddcl  9450  fseq1p1m1  9888  modqmuladdim  10154  frec2uzrand  10192  frecuzrdglem  10198  frecuzrdg0  10200  frecuzrdgdomlem  10204  frecuzrdg0t  10209  frecuzrdgsuctlem  10210  seq3val  10245  seq3feq  10259  iseqf1olemnab  10275  seqfeq3  10299  expaddzaplem  10350  expaddzap  10351  expmulzap  10353  zesq  10424  bcm1k  10520  bccl  10527  permnn  10531  seq3coll  10599  shftuz  10603  ref  10641  imf  10642  crre  10643  rereb  10649  resqrexlemnm  10804  absf  10896  summodclem2a  11164  summodc  11166  fsumgcl  11169  fsum3  11170  fsumf1o  11173  fsumcnv  11220  mptfzshft  11225  isumlessdc  11279  geolim2  11295  prodmodclem3  11358  oexpneg  11587  nn0ob  11618  divalglemqt  11629  gcdf  11674  lcmgcdlem  11771  sqnprm  11829  sqrt2irrlem  11852  2sqpwodd  11867  fnum  11881  fden  11882  phimullem  11914  ctiunctlemfo  11965  unopn  12188  tsettps  12221  tgss2  12264  difopn  12293  resttop  12355  resttopon  12356  restco  12359  tgcn  12393  tgcnp  12394  cnptopco  12407  upxp  12457  txcn  12460  txdis  12462  cnmpt11  12468  cnmpt11f  12469  cnmpt1t  12470  cnmpt12  12472  cnmpt21  12476  cnmpt21f  12477  cnmpt2t  12478  cnmpt22  12479  cnmpt22f  12480  cnmpt1res  12481  xmeter  12621  mscl  12650  xmscl  12651  bdxmet  12686  cncfmpt1f  12769  cdivcncfap  12772  negfcncf  12774  cnmptlimc  12828  dvcnp2cntop  12848  sincn  12875  coscn  12876  relogcl  12967  pwtrufal  13299
  Copyright terms: Public domain W3C validator