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

Theorem eqeltrrd 2244
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 2171 . 2 (𝜑𝐵 = 𝐴)
3 eqeltrrd.2 . 2 (𝜑𝐴𝐶)
42, 3eqeltrd 2243 1 (𝜑𝐵𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1343  wcel 2136
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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147
This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161
This theorem is referenced by:  3eltr3d  2249  exmid01  4177  pwntru  4178  xpexr2m  5045  funimaexg  5272  fvmptdv2  5575  ffvresb  5648  2ndrn  6151  1st2ndbr  6152  elopabi  6163  cnvf1olem  6192  dftpos4  6231  tfrlemibxssdm  6295  tfr1onlembxssdm  6311  tfrcllembxssdm  6324  nnmordi  6484  th3qlem1  6603  infiexmid  6843  onunsnss  6882  ssfirab  6899  ssfidc  6900  fnfi  6902  fidcenumlemr  6920  elfi2  6937  ordiso2  7000  djulclb  7020  ctmlemr  7073  ctssdccl  7076  ctssdc  7078  exmidfodomrlemreseldju  7156  exmidfodomrlemr  7158  archnqq  7358  prarloclemarch2  7360  enq0tr  7375  nqnq0  7382  addcmpblnq0  7384  mulcmpblnq0  7385  mulcanenq0ec  7386  addclnq0  7392  mulclnq0  7393  nqpnq0nq  7394  nq0m0r  7397  distrnq0  7400  addassnq0lemcl  7402  prarloclemlt  7434  prarloclem5  7441  distrlem4prl  7525  distrlem4pru  7526  ltexprlemm  7541  ltexprlemrl  7551  ltexprlemru  7553  addcanprleml  7555  cauappcvgprlemladdru  7597  prsrlem1  7683  mulgt0sr  7719  axpre-suploclemres  7842  cnegexlem2  8074  subf  8100  resubcl  8162  negcon1ad  8204  subeq0bd  8277  rimul  8483  rereim  8484  aprcl  8544  nn0nnaddcl  9145  elnn0nn  9156  zaddcllemneg  9230  zsubcl  9232  zrevaddcl  9241  elz2  9262  zdiv  9279  peano5uzti  9299  peano2uzr  9523  uzaddcl  9524  divfnzn  9559  qsubcl  9576  qrevaddcl  9582  fseq1p1m1  10029  modqmuladdim  10302  frec2uzrand  10340  frecuzrdglem  10346  frecuzrdg0  10348  frecuzrdgdomlem  10352  frecuzrdg0t  10357  frecuzrdgsuctlem  10358  seq3val  10393  seq3feq  10407  iseqf1olemnab  10423  seqfeq3  10447  expaddzaplem  10498  expaddzap  10499  expmulzap  10501  zesq  10573  bcm1k  10673  bccl  10680  permnn  10684  seq3coll  10755  shftuz  10759  ref  10797  imf  10798  crre  10799  rereb  10805  resqrexlemnm  10960  absf  11052  summodclem2a  11322  summodc  11324  fsumgcl  11327  fsum3  11328  fsumf1o  11331  fsumcnv  11378  mptfzshft  11383  isumlessdc  11437  geolim2  11453  prodmodclem3  11516  fprodseq  11524  fprodf1o  11529  oexpneg  11814  nn0ob  11845  divalglemqt  11856  suprzubdc  11885  gcdf  11905  lcmgcdlem  12009  sqnprm  12068  sqrt2irrlem  12093  2sqpwodd  12108  fnum  12122  fden  12123  phimullem  12157  pc2dvds  12261  gzsubcl  12310  4sqlem5  12312  4sqlem9  12316  4sqlem10  12317  mul4sqlem  12323  mul4sq  12324  ctiunctlemfo  12372  mgmsscl  12592  unopn  12643  tsettps  12676  tgss2  12719  difopn  12748  resttop  12810  resttopon  12811  restco  12814  tgcn  12848  tgcnp  12849  cnptopco  12862  upxp  12912  txcn  12915  txdis  12917  cnmpt11  12923  cnmpt11f  12924  cnmpt1t  12925  cnmpt12  12927  cnmpt21  12931  cnmpt21f  12932  cnmpt2t  12933  cnmpt22  12934  cnmpt22f  12935  cnmpt1res  12936  xmeter  13076  mscl  13105  xmscl  13106  bdxmet  13141  cncfmpt1f  13224  cdivcncfap  13227  negfcncf  13229  cnmptlimc  13283  dvcnp2cntop  13303  sincn  13330  coscn  13331  relogcl  13423  lgsne0  13579  pwtrufal  13877
  Copyright terms: Public domain W3C validator