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

Theorem eqeltrrd 2160
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 2088 . 2 (𝜑𝐵 = 𝐴)
3 eqeltrrd.2 . 2 (𝜑𝐴𝐶)
42, 3eqeltrd 2159 1 (𝜑𝐵𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1285  wcel 1434
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-cleq 2076  df-clel 2079
This theorem is referenced by:  3eltr3d  2165  exmid01  3988  xpexr2m  4812  funimaexg  5034  fvmptdv2  5313  ffvresb  5381  2ndrn  5861  1st2ndbr  5862  elopabi  5873  cnvf1olem  5897  dftpos4  5933  tfrlemibxssdm  5997  tfr1onlembxssdm  6013  tfrcllembxssdm  6026  nnmordi  6177  th3qlem1  6296  infiexmid  6434  onunsnss  6462  ssfirab  6476  ssfidc  6477  fnfi  6479  ordiso2  6541  djuun  6568  archnqq  6739  prarloclemarch2  6741  enq0tr  6756  nqnq0  6763  addcmpblnq0  6765  mulcmpblnq0  6766  mulcanenq0ec  6767  addclnq0  6773  mulclnq0  6774  nqpnq0nq  6775  nq0m0r  6778  distrnq0  6781  addassnq0lemcl  6783  prarloclemlt  6815  prarloclem5  6822  distrlem4prl  6906  distrlem4pru  6907  ltexprlemm  6922  ltexprlemrl  6932  ltexprlemru  6934  addcanprleml  6936  cauappcvgprlemladdru  6978  prsrlem1  7051  mulgt0sr  7086  cnegexlem2  7421  subf  7447  resubcl  7509  negcon1ad  7551  subeq0bd  7620  rimul  7822  rereim  7823  nn0nnaddcl  8456  elnn0nn  8467  zaddcllemneg  8541  zsubcl  8543  zrevaddcl  8552  elz2  8570  zdiv  8586  peano5uzti  8606  peano2uzr  8824  uzaddcl  8825  divfnzn  8857  qsubcl  8874  qrevaddcl  8880  fseq1p1m1  9257  modqmuladdim  9519  frec2uzrand  9557  frecuzrdglem  9563  frecuzrdg0  9565  frecuzrdgdomlem  9569  frecuzrdg0t  9574  frecuzrdgsuctlem  9575  iseqvalt  9602  iseqfeq  9617  iseqdistr  9637  serige0  9640  serile  9641  expaddzaplem  9686  expaddzap  9687  expmulzap  9689  zesq  9758  bcm1k  9854  bccl  9861  permnn  9865  shftuz  9924  ref  9961  imf  9962  crre  9963  rereb  9969  resqrexlemnm  10123  absf  10215  iserile  10399  oexpneg  10502  nn0ob  10533  divalglemqt  10544  gcdf  10589  lcmgcdlem  10684  sqnprm  10742  sqrt2irrlem  10765  2sqpwodd  10779  fnum  10793  fden  10794  phimullem  10826
  Copyright terms: Public domain W3C validator