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

Theorem eqeltrrd 2162
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 2090 . 2 (𝜑𝐵 = 𝐴)
3 eqeltrrd.2 . 2 (𝜑𝐴𝐶)
42, 3eqeltrd 2161 1 (𝜑𝐵𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1287  wcel 1436
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 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078  df-clel 2081
This theorem is referenced by:  3eltr3d  2167  exmid01  4005  xpexr2m  4835  funimaexg  5060  fvmptdv2  5349  ffvresb  5418  2ndrn  5904  1st2ndbr  5905  elopabi  5916  cnvf1olem  5940  dftpos4  5976  tfrlemibxssdm  6040  tfr1onlembxssdm  6056  tfrcllembxssdm  6069  nnmordi  6221  th3qlem1  6340  infiexmid  6539  onunsnss  6573  ssfirab  6587  ssfidc  6588  fnfi  6590  ordiso2  6665  djulclb  6684  exmidfodomrlemreseldju  6763  exmidfodomrlemr  6765  archnqq  6913  prarloclemarch2  6915  enq0tr  6930  nqnq0  6937  addcmpblnq0  6939  mulcmpblnq0  6940  mulcanenq0ec  6941  addclnq0  6947  mulclnq0  6948  nqpnq0nq  6949  nq0m0r  6952  distrnq0  6955  addassnq0lemcl  6957  prarloclemlt  6989  prarloclem5  6996  distrlem4prl  7080  distrlem4pru  7081  ltexprlemm  7096  ltexprlemrl  7106  ltexprlemru  7108  addcanprleml  7110  cauappcvgprlemladdru  7152  prsrlem1  7225  mulgt0sr  7260  cnegexlem2  7595  subf  7621  resubcl  7683  negcon1ad  7725  subeq0bd  7794  rimul  7996  rereim  7997  nn0nnaddcl  8630  elnn0nn  8641  zaddcllemneg  8715  zsubcl  8717  zrevaddcl  8726  elz2  8744  zdiv  8760  peano5uzti  8780  peano2uzr  8998  uzaddcl  8999  divfnzn  9031  qsubcl  9048  qrevaddcl  9054  fseq1p1m1  9431  modqmuladdim  9695  frec2uzrand  9733  frecuzrdglem  9739  frecuzrdg0  9741  frecuzrdgdomlem  9745  frecuzrdg0t  9750  frecuzrdgsuctlem  9751  iseqvalt  9783  iseqfeq  9798  iseqf1olemnab  9814  iseqdistr  9839  serige0  9843  serile  9844  expaddzaplem  9889  expaddzap  9890  expmulzap  9892  zesq  9961  bcm1k  10057  bccl  10064  permnn  10068  iseqcoll  10136  shftuz  10140  ref  10177  imf  10178  crre  10179  rereb  10185  resqrexlemnm  10339  absf  10431  iserile  10615  isummolem2a  10653  isummo  10655  fisum  10658  fsumf1o  10661  oexpneg  10744  nn0ob  10775  divalglemqt  10786  gcdf  10831  lcmgcdlem  10926  sqnprm  10984  sqrt2irrlem  11007  2sqpwodd  11021  fnum  11035  fden  11036  phimullem  11068
  Copyright terms: Public domain W3C validator