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

Theorem eqeltrrd 2195
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 2123 . 2  |-  ( ph  ->  B  =  A )
3 eqeltrrd.2 . 2  |-  ( ph  ->  A  e.  C )
42, 3eqeltrd 2194 1  |-  ( ph  ->  B  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:  3eltr3d  2200  exmid01  4091  pwntru  4092  xpexr2m  4950  funimaexg  5177  fvmptdv2  5478  ffvresb  5551  2ndrn  6049  1st2ndbr  6050  elopabi  6061  cnvf1olem  6089  dftpos4  6128  tfrlemibxssdm  6192  tfr1onlembxssdm  6208  tfrcllembxssdm  6221  nnmordi  6380  th3qlem1  6499  infiexmid  6739  onunsnss  6773  ssfirab  6790  ssfidc  6791  fnfi  6793  fidcenumlemr  6811  elfi2  6828  ordiso2  6888  djulclb  6908  ctmlemr  6961  ctssdccl  6964  ctssdc  6966  exmidfodomrlemreseldju  7024  exmidfodomrlemr  7026  archnqq  7193  prarloclemarch2  7195  enq0tr  7210  nqnq0  7217  addcmpblnq0  7219  mulcmpblnq0  7220  mulcanenq0ec  7221  addclnq0  7227  mulclnq0  7228  nqpnq0nq  7229  nq0m0r  7232  distrnq0  7235  addassnq0lemcl  7237  prarloclemlt  7269  prarloclem5  7276  distrlem4prl  7360  distrlem4pru  7361  ltexprlemm  7376  ltexprlemrl  7386  ltexprlemru  7388  addcanprleml  7390  cauappcvgprlemladdru  7432  prsrlem1  7518  mulgt0sr  7554  axpre-suploclemres  7677  cnegexlem2  7906  subf  7932  resubcl  7994  negcon1ad  8036  subeq0bd  8109  rimul  8314  rereim  8315  aprcl  8375  nn0nnaddcl  8966  elnn0nn  8977  zaddcllemneg  9051  zsubcl  9053  zrevaddcl  9062  elz2  9080  zdiv  9097  peano5uzti  9117  peano2uzr  9336  uzaddcl  9337  divfnzn  9369  qsubcl  9386  qrevaddcl  9392  fseq1p1m1  9829  modqmuladdim  10095  frec2uzrand  10133  frecuzrdglem  10139  frecuzrdg0  10141  frecuzrdgdomlem  10145  frecuzrdg0t  10150  frecuzrdgsuctlem  10151  seq3val  10186  seq3feq  10200  iseqf1olemnab  10216  seqfeq3  10240  expaddzaplem  10291  expaddzap  10292  expmulzap  10294  zesq  10365  bcm1k  10461  bccl  10468  permnn  10472  seq3coll  10540  shftuz  10544  ref  10582  imf  10583  crre  10584  rereb  10590  resqrexlemnm  10745  absf  10837  summodclem2a  11105  summodc  11107  fsumgcl  11110  fsum3  11111  fsumf1o  11114  fsumcnv  11161  mptfzshft  11166  isumlessdc  11220  geolim2  11236  oexpneg  11486  nn0ob  11517  divalglemqt  11528  gcdf  11573  lcmgcdlem  11670  sqnprm  11728  sqrt2irrlem  11751  2sqpwodd  11765  fnum  11779  fden  11780  phimullem  11812  ctiunctlemfo  11863  unopn  12083  tsettps  12116  tgss2  12159  difopn  12188  resttop  12250  resttopon  12251  restco  12254  tgcn  12288  tgcnp  12289  cnptopco  12302  upxp  12352  txcn  12355  txdis  12357  cnmpt11  12363  cnmpt11f  12364  cnmpt1t  12365  cnmpt12  12367  cnmpt21  12371  cnmpt21f  12372  cnmpt2t  12373  cnmpt22  12374  cnmpt22f  12375  cnmpt1res  12376  xmeter  12516  mscl  12545  xmscl  12546  bdxmet  12581  cncfmpt1f  12664  cdivcncfap  12667  negfcncf  12669  cnmptlimc  12723  dvcnp2cntop  12743  sincn  12769  coscn  12770  pwtrufal  13088
  Copyright terms: Public domain W3C validator