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

Theorem eqeltrrd 2218
Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
Hypotheses
Ref Expression
eqeltrrd.1 (𝜑𝐴 = 𝐵)
eqeltrrd.2 (𝜑𝐴𝐶)
Assertion
Ref Expression
eqeltrrd (𝜑𝐵𝐶)

Proof of Theorem eqeltrrd
StepHypRef Expression
1 eqeltrrd.1 . . 3 (𝜑𝐴 = 𝐵)
21eqcomd 2146 . 2 (𝜑𝐵 = 𝐴)
3 eqeltrrd.2 . 2 (𝜑𝐴𝐶)
42, 3eqeltrd 2217 1 (𝜑𝐵𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1332  wcel 1481
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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136
This theorem is referenced by:  3eltr3d  2223  exmid01  4128  pwntru  4129  xpexr2m  4987  funimaexg  5214  fvmptdv2  5517  ffvresb  5590  2ndrn  6088  1st2ndbr  6089  elopabi  6100  cnvf1olem  6128  dftpos4  6167  tfrlemibxssdm  6231  tfr1onlembxssdm  6247  tfrcllembxssdm  6260  nnmordi  6419  th3qlem1  6538  infiexmid  6778  onunsnss  6812  ssfirab  6829  ssfidc  6830  fnfi  6832  fidcenumlemr  6850  elfi2  6867  ordiso2  6927  djulclb  6947  ctmlemr  7000  ctssdccl  7003  ctssdc  7005  exmidfodomrlemreseldju  7072  exmidfodomrlemr  7074  archnqq  7248  prarloclemarch2  7250  enq0tr  7265  nqnq0  7272  addcmpblnq0  7274  mulcmpblnq0  7275  mulcanenq0ec  7276  addclnq0  7282  mulclnq0  7283  nqpnq0nq  7284  nq0m0r  7287  distrnq0  7290  addassnq0lemcl  7292  prarloclemlt  7324  prarloclem5  7331  distrlem4prl  7415  distrlem4pru  7416  ltexprlemm  7431  ltexprlemrl  7441  ltexprlemru  7443  addcanprleml  7445  cauappcvgprlemladdru  7487  prsrlem1  7573  mulgt0sr  7609  axpre-suploclemres  7732  cnegexlem2  7961  subf  7987  resubcl  8049  negcon1ad  8091  subeq0bd  8164  rimul  8370  rereim  8371  aprcl  8431  nn0nnaddcl  9031  elnn0nn  9042  zaddcllemneg  9116  zsubcl  9118  zrevaddcl  9127  elz2  9145  zdiv  9162  peano5uzti  9182  peano2uzr  9406  uzaddcl  9407  divfnzn  9439  qsubcl  9456  qrevaddcl  9462  fseq1p1m1  9904  modqmuladdim  10170  frec2uzrand  10208  frecuzrdglem  10214  frecuzrdg0  10216  frecuzrdgdomlem  10220  frecuzrdg0t  10225  frecuzrdgsuctlem  10226  seq3val  10261  seq3feq  10275  iseqf1olemnab  10291  seqfeq3  10315  expaddzaplem  10366  expaddzap  10367  expmulzap  10369  zesq  10440  bcm1k  10537  bccl  10544  permnn  10548  seq3coll  10616  shftuz  10620  ref  10658  imf  10659  crre  10660  rereb  10666  resqrexlemnm  10821  absf  10913  summodclem2a  11181  summodc  11183  fsumgcl  11186  fsum3  11187  fsumf1o  11190  fsumcnv  11237  mptfzshft  11242  isumlessdc  11296  geolim2  11312  prodmodclem3  11375  oexpneg  11608  nn0ob  11639  divalglemqt  11650  gcdf  11695  lcmgcdlem  11792  sqnprm  11850  sqrt2irrlem  11873  2sqpwodd  11888  fnum  11902  fden  11903  phimullem  11935  ctiunctlemfo  11986  unopn  12209  tsettps  12242  tgss2  12285  difopn  12314  resttop  12376  resttopon  12377  restco  12380  tgcn  12414  tgcnp  12415  cnptopco  12428  upxp  12478  txcn  12481  txdis  12483  cnmpt11  12489  cnmpt11f  12490  cnmpt1t  12491  cnmpt12  12493  cnmpt21  12497  cnmpt21f  12498  cnmpt2t  12499  cnmpt22  12500  cnmpt22f  12501  cnmpt1res  12502  xmeter  12642  mscl  12671  xmscl  12672  bdxmet  12707  cncfmpt1f  12790  cdivcncfap  12793  negfcncf  12795  cnmptlimc  12849  dvcnp2cntop  12869  sincn  12896  coscn  12897  relogcl  12989  pwtrufal  13363
  Copyright terms: Public domain W3C validator