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

Theorem csbeq1a 2983
Description: Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
Assertion
Ref Expression
csbeq1a (𝑥 = 𝐴𝐵 = 𝐴 / 𝑥𝐵)

Proof of Theorem csbeq1a
StepHypRef Expression
1 csbid 2982 . 2 𝑥 / 𝑥𝐵 = 𝐵
2 csbeq1 2978 . 2 (𝑥 = 𝐴𝑥 / 𝑥𝐵 = 𝐴 / 𝑥𝐵)
31, 2syl5eqr 2164 1 (𝑥 = 𝐴𝐵 = 𝐴 / 𝑥𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1316  csb 2975
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-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-11 1469  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-sbc 2883  df-csb 2976
This theorem is referenced by:  csbhypf  3008  csbiebt  3009  sbcnestgf  3021  cbvralcsf  3032  cbvrexcsf  3033  cbvreucsf  3034  cbvrabcsf  3035  csbing  3253  disjnims  3891  disjiun  3894  sbcbrg  3952  moop2  4143  pofun  4204  eusvnf  4344  opeliunxp  4564  elrnmpt1  4760  resmptf  4839  csbima12g  4870  fvmpts  5467  fvmpt2  5472  mptfvex  5474  fmptco  5554  fmptcof  5555  fmptcos  5556  elabrex  5627  fliftfuns  5667  csbov123g  5777  ovmpos  5862  csbopeq1a  6054  mpomptsx  6063  dmmpossx  6065  fmpox  6066  mpofvex  6069  fmpoco  6081  disjxp1  6101  eqerlem  6428  qliftfuns  6481  mptelixpg  6596  xpf1o  6706  iunfidisj  6802  seq3f1olemstep  10229  seq3f1olemp  10230  sumeq2  11083  sumfct  11098  sumrbdclem  11100  summodclem3  11104  summodclem2a  11105  zsumdc  11108  fsumgcl  11110  fsum3  11111  isumss  11115  isumss2  11117  fsum3cvg2  11118  fsumzcl2  11129  fsumsplitf  11132  sumsnf  11133  sumsns  11139  fsumsplitsnun  11143  fsum2dlemstep  11158  fsumcnv  11161  fisumcom2  11162  fsumshftm  11169  fisum0diag2  11171  fsummulc2  11172  fsum00  11186  fsumabs  11189  fsumrelem  11195  fsumiun  11201  isumshft  11214  mertenslem2  11260  ctiunctlemudc  11861  ctiunctlemf  11862  iuncld  12195  fsumcncntop  12636  limcmpted  12712
  Copyright terms: Public domain W3C validator