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  8315  rereim  8316  aprcl  8376  nn0nnaddcl  8976  elnn0nn  8987  zaddcllemneg  9061  zsubcl  9063  zrevaddcl  9072  elz2  9090  zdiv  9107  peano5uzti  9127  peano2uzr  9348  uzaddcl  9349  divfnzn  9381  qsubcl  9398  qrevaddcl  9404  fseq1p1m1  9842  modqmuladdim  10108  frec2uzrand  10146  frecuzrdglem  10152  frecuzrdg0  10154  frecuzrdgdomlem  10158  frecuzrdg0t  10163  frecuzrdgsuctlem  10164  seq3val  10199  seq3feq  10213  iseqf1olemnab  10229  seqfeq3  10253  expaddzaplem  10304  expaddzap  10305  expmulzap  10307  zesq  10378  bcm1k  10474  bccl  10481  permnn  10485  seq3coll  10553  shftuz  10557  ref  10595  imf  10596  crre  10597  rereb  10603  resqrexlemnm  10758  absf  10850  summodclem2a  11118  summodc  11120  fsumgcl  11123  fsum3  11124  fsumf1o  11127  fsumcnv  11174  mptfzshft  11179  isumlessdc  11233  geolim2  11249  oexpneg  11501  nn0ob  11532  divalglemqt  11543  gcdf  11588  lcmgcdlem  11685  sqnprm  11743  sqrt2irrlem  11766  2sqpwodd  11781  fnum  11795  fden  11796  phimullem  11828  ctiunctlemfo  11879  unopn  12099  tsettps  12132  tgss2  12175  difopn  12204  resttop  12266  resttopon  12267  restco  12270  tgcn  12304  tgcnp  12305  cnptopco  12318  upxp  12368  txcn  12371  txdis  12373  cnmpt11  12379  cnmpt11f  12380  cnmpt1t  12381  cnmpt12  12383  cnmpt21  12387  cnmpt21f  12388  cnmpt2t  12389  cnmpt22  12390  cnmpt22f  12391  cnmpt1res  12392  xmeter  12532  mscl  12561  xmscl  12562  bdxmet  12597  cncfmpt1f  12680  cdivcncfap  12683  negfcncf  12685  cnmptlimc  12739  dvcnp2cntop  12759  sincn  12785  coscn  12786  pwtrufal  13119
  Copyright terms: Public domain W3C validator