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

Theorem eqeltri 2188
Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eqeltr.1 𝐴 = 𝐵
eqeltr.2 𝐵𝐶
Assertion
Ref Expression
eqeltri 𝐴𝐶

Proof of Theorem eqeltri
StepHypRef Expression
1 eqeltr.2 . 2 𝐵𝐶
2 eqeltr.1 . . 3 𝐴 = 𝐵
32eleq1i 2181 . 2 (𝐴𝐶𝐵𝐶)
41, 3mpbir 145 1 𝐴𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1314  wcel 1463
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 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-clel 2111
This theorem is referenced by:  eqeltrri  2189  3eltr4i  2197  intab  3768  inex2  4031  vpwex  4071  ord3ex  4082  uniopel  4146  onsucelsucexmid  4413  nnpredcl  4504  elvvuni  4571  isarep2  5178  acexmidlemcase  5735  abrexex2  5988  oprabex  5992  oprabrexex2  5994  rdg0  6250  frecex  6257  1on  6286  2on  6288  3on  6290  4on  6291  1onn  6382  2onn  6383  3onn  6384  4onn  6385  mapsnf1o2  6556  exmidpw  6768  unfiexmid  6772  xpfi  6784  ssfirab  6788  fnfi  6791  iunfidisj  6800  fidcenumlemr  6809  sbthlemi10  6820  ctmlemr  6959  acfun  7027  exmidaclem  7028  ccfunen  7043  nqex  7135  nq0ex  7212  1pr  7326  ltexprlempr  7380  recexprlempr  7404  cauappcvgprlemcl  7425  caucvgprlemcl  7448  caucvgprprlemcl  7476  addvalex  7616  peano1nnnn  7624  peano2nnnn  7625  axcnex  7631  ax1cn  7633  ax1re  7634  pnfxr  7782  mnfxr  7786  inelr  8309  cju  8679  2re  8750  3re  8754  4re  8757  5re  8759  6re  8761  7re  8763  8re  8765  9re  8767  2nn  8835  3nn  8836  4nn  8837  5nn  8838  6nn  8839  7nn  8840  8nn  8841  9nn  8842  nn0ex  8937  nneoor  9107  zeo  9110  deccl  9150  decnncl  9155  numnncl2  9158  decnncl2  9159  numsucc  9175  numma2c  9181  numadd  9182  numaddc  9183  nummul1c  9184  nummul2c  9185  xnegcl  9566  xrex  9590  ioof  9705  uzennn  10160  seqex  10171  m1expcl2  10266  faccl  10432  facwordi  10437  faclbnd2  10439  bccl  10464  crre  10580  remim  10583  absval  10724  climle  11054  climcvg1nlem  11069  iserabs  11195  geo2lim  11236  ere  11286  ege2le3  11287  eftlub  11306  efsep  11307  tan0  11348  ef01bndlem  11373  nn0o  11511  ennnfonelemj0  11820  ennnfonelem0  11824  ndxarg  11888  ndxslid  11890  strndxid  11893  basendxnn  11920  strle1g  11955  2strbasg  11966  2stropg  11967  setsmsbasg  12554  cnbl0  12609  cnopncntop  12612  remet  12615  divcnap  12630  climcncf  12646  expcncf  12667  cnrehmeocntop  12668  sincn  12764  coscn  12765  bdinex2  12932  bj-inex  12939  peano3nninf  13035  nninfex  13039  isomninnlem  13059  cvgcmp2nlemabs  13061  trilpolemisumle  13065
  Copyright terms: Public domain W3C validator