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

Theorem eqeltrrd 2131
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 2061 . 2 (𝜑𝐵 = 𝐴)
3 eqeltrrd.2 . 2 (𝜑𝐴𝐶)
42, 3eqeltrd 2130 1 (𝜑𝐵𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1259  wcel 1409
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049  df-clel 2052
This theorem is referenced by:  3eltr3d  2136  xpexr2m  4789  funimaexg  5010  fvmptdv2  5287  ffvresb  5355  2ndrn  5836  1st2ndbr  5837  elopabi  5848  cnvf1olem  5872  dftpos4  5908  tfrlemibxssdm  5971  nnmordi  6119  th3qlem1  6238  onunsnss  6385  ordiso2  6414  archnqq  6572  prarloclemarch2  6574  enq0tr  6589  nqnq0  6596  addcmpblnq0  6598  mulcmpblnq0  6599  mulcanenq0ec  6600  addclnq0  6606  mulclnq0  6607  nqpnq0nq  6608  nq0m0r  6611  distrnq0  6614  addassnq0lemcl  6616  prarloclemlt  6648  prarloclem5  6655  distrlem4prl  6739  distrlem4pru  6740  ltexprlemm  6755  ltexprlemrl  6765  ltexprlemru  6767  addcanprleml  6769  cauappcvgprlemladdru  6811  prsrlem1  6884  mulgt0sr  6919  cnegexlem2  7249  subf  7275  resubcl  7337  negcon1ad  7379  subeq0bd  7448  rimul  7649  rereim  7650  nn0nnaddcl  8269  elnn0nn  8280  zaddcllemneg  8340  zsubcl  8342  zrevaddcl  8351  elz2  8369  zdiv  8385  peano5uzti  8404  peano2uzr  8623  uzaddcl  8624  divfnzn  8652  qsubcl  8669  qrevaddcl  8675  fseq1p1m1  9057  modqmuladdim  9316  frec2uzrand  9354  frecuzrdglem  9360  frecuzrdg0  9363  iseqfeq  9394  iseqdistr  9413  serige0  9416  serile  9417  expaddzaplem  9462  expaddzap  9463  expmulzap  9465  zesq  9534  bcm1k  9627  bccl  9634  permnn  9638  shftuz  9645  ref  9682  imf  9683  crre  9684  rereb  9690  resqrexlemnm  9844  absf  9936  iserile  10092  oexpneg  10187  nn0ob  10219  sqr2irrlem  10229
  Copyright terms: Public domain W3C validator