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

Theorem eqeltri 2190
Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eqeltr.1  |-  A  =  B
eqeltr.2  |-  B  e.  C
Assertion
Ref Expression
eqeltri  |-  A  e.  C

Proof of Theorem eqeltri
StepHypRef Expression
1 eqeltr.2 . 2  |-  B  e.  C
2 eqeltr.1 . . 3  |-  A  =  B
32eleq1i 2183 . 2  |-  ( A  e.  C  <->  B  e.  C )
41, 3mpbir 145 1  |-  A  e.  C
Colors of variables: wff set class
Syntax hints:    = wceq 1316    e. wcel 1465
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 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110  df-clel 2113
This theorem is referenced by:  eqeltrri  2191  3eltr4i  2199  intab  3770  inex2  4033  vpwex  4073  ord3ex  4084  uniopel  4148  onsucelsucexmid  4415  nnpredcl  4506  elvvuni  4573  isarep2  5180  acexmidlemcase  5737  abrexex2  5990  oprabex  5994  oprabrexex2  5996  rdg0  6252  frecex  6259  1on  6288  2on  6290  3on  6292  4on  6293  1onn  6384  2onn  6385  3onn  6386  4onn  6387  mapsnf1o2  6558  exmidpw  6770  unfiexmid  6774  xpfi  6786  ssfirab  6790  fnfi  6793  iunfidisj  6802  fidcenumlemr  6811  sbthlemi10  6822  ctmlemr  6961  exmidonfinlem  7017  acfun  7031  exmidaclem  7032  ccfunen  7047  nqex  7139  nq0ex  7216  1pr  7330  ltexprlempr  7384  recexprlempr  7408  cauappcvgprlemcl  7429  caucvgprlemcl  7452  caucvgprprlemcl  7480  addvalex  7620  peano1nnnn  7628  peano2nnnn  7629  axcnex  7635  ax1cn  7637  ax1re  7638  pnfxr  7786  mnfxr  7790  inelr  8314  cju  8687  2re  8758  3re  8762  4re  8765  5re  8767  6re  8769  7re  8771  8re  8773  9re  8775  2nn  8849  3nn  8850  4nn  8851  5nn  8852  6nn  8853  7nn  8854  8nn  8855  9nn  8856  nn0ex  8951  nneoor  9121  zeo  9124  deccl  9164  decnncl  9169  numnncl2  9172  decnncl2  9173  numsucc  9189  numma2c  9195  numadd  9196  numaddc  9197  nummul1c  9198  nummul2c  9199  xnegcl  9583  xrex  9607  ioof  9722  uzennn  10177  seqex  10188  m1expcl2  10283  faccl  10449  facwordi  10454  faclbnd2  10456  bccl  10481  crre  10597  remim  10600  absval  10741  climle  11071  climcvg1nlem  11086  iserabs  11212  geo2lim  11253  ere  11303  ege2le3  11304  eftlub  11323  efsep  11324  tan0  11365  ef01bndlem  11390  nn0o  11531  ennnfonelemj0  11841  ennnfonelem0  11845  ndxarg  11909  ndxslid  11911  strndxid  11914  basendxnn  11941  strle1g  11976  2strbasg  11987  2stropg  11988  setsmsbasg  12575  cnbl0  12630  cnopncntop  12633  remet  12636  divcnap  12651  climcncf  12667  expcncf  12688  cnrehmeocntop  12689  sincn  12785  coscn  12786  bdinex2  13025  bj-inex  13032  peano3nninf  13128  nninfex  13132  isomninnlem  13152  cvgcmp2nlemabs  13154  trilpolemisumle  13158
  Copyright terms: Public domain W3C validator