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

Theorem csbeq1a 3066
Description: Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
Assertion
Ref Expression
csbeq1a  |-  ( x  =  A  ->  B  =  [_ A  /  x ]_ B )

Proof of Theorem csbeq1a
StepHypRef Expression
1 csbid 3065 . 2  |-  [_ x  /  x ]_ B  =  B
2 csbeq1 3060 . 2  |-  ( x  =  A  ->  [_ x  /  x ]_ B  = 
[_ A  /  x ]_ B )
31, 2eqtr3id 2224 1  |-  ( x  =  A  ->  B  =  [_ A  /  x ]_ B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1353   [_csb 3057
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-sbc 2963  df-csb 3058
This theorem is referenced by:  csbhypf  3095  csbiebt  3096  sbcnestgf  3108  cbvralcsf  3119  cbvrexcsf  3120  cbvreucsf  3121  cbvrabcsf  3122  rspc2vd  3125  csbing  3342  disjnims  3992  disjiun  3995  sbcbrg  4054  moop2  4247  pofun  4308  eusvnf  4449  opeliunxp  4677  elrnmpt1  4873  resmptf  4952  csbima12g  4984  fvmpts  5589  fvmpt2  5594  mptfvex  5596  fmptco  5677  fmptcof  5678  fmptcos  5679  elabrex  5752  fliftfuns  5792  csbov123g  5906  ovmpos  5991  csbopeq1a  6182  mpomptsx  6191  dmmpossx  6193  fmpox  6194  mpofvex  6197  fmpoco  6210  disjxp1  6230  eqerlem  6559  qliftfuns  6612  mptelixpg  6727  xpf1o  6837  iunfidisj  6938  cc3  7245  seq3f1olemstep  10474  seq3f1olemp  10475  sumeq2  11338  sumfct  11353  sumrbdclem  11356  summodclem3  11359  summodclem2a  11360  zsumdc  11363  fsumgcl  11365  fsum3  11366  isumss  11370  isumss2  11372  fsum3cvg2  11373  fsumzcl2  11384  fsumsplitf  11387  sumsnf  11388  sumsns  11394  fsumsplitsnun  11398  fsum2dlemstep  11413  fsumcnv  11416  fisumcom2  11417  fsumshftm  11424  fisum0diag2  11426  fsummulc2  11427  fsum00  11441  fsumabs  11444  fsumrelem  11450  fsumiun  11456  isumshft  11469  mertenslem2  11515  prodeq2  11536  prodrbdclem  11550  prodmodclem3  11554  prodmodclem2a  11555  zproddc  11558  fprodseq  11562  fprodntrivap  11563  prodfct  11566  prodssdc  11568  fprodmul  11570  prodsnf  11571  fprodm1s  11580  fprodp1s  11581  prodsns  11582  fprodcl2lem  11584  fprodcllemf  11592  fprodabs  11595  fprodap0  11600  fprod2dlemstep  11601  fprodcnv  11604  fprodcom2fi  11605  fprodrec  11608  fproddivapf  11610  fprodsplitf  11611  fprodsplit1f  11613  fprodap0f  11615  fprodle  11619  fprodmodd  11620  pcmpt  12311  pcmptdvds  12313  ctiunctlemudc  12408  ctiunctlemf  12409  ctiunctal  12412  iuncld  13248  fsumcncntop  13689  limcmpted  13765
  Copyright terms: Public domain W3C validator