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

Theorem csbeq1 2832
Description: Analog of dfsbcq 2743 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
Assertion
Ref Expression
csbeq1 (A = BA / x𝐶 = B / x𝐶)

Proof of Theorem csbeq1
Dummy variable y is distinct from all other variables.
StepHypRef Expression
1 dfsbcq 2743 . . 3 (A = B → ([A / x]y 𝐶[B / x]y 𝐶))
21abbidv 2137 . 2 (A = B → {y[A / x]y 𝐶} = {y[B / x]y 𝐶})
3 df-csb 2830 . 2 A / x𝐶 = {y[A / x]y 𝐶}
4 df-csb 2830 . 2 B / x𝐶 = {y[B / x]y 𝐶}
52, 3, 43eqtr4g 2079 1 (A = BA / x𝐶 = B / x𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1228   wcel 1374  {cab 2008  [wsbc 2741  csb 2829
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-11 1378  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-tru 1231  df-nf 1330  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-sbc 2742  df-csb 2830
This theorem is referenced by:  csbeq1d  2835  csbeq1a  2837  csbiebg  2866  sbcnestgf  2874  cbvralcsf  2885  cbvrexcsf  2886  cbvreucsf  2887  cbvrabcsf  2888  csbing  3121  sbcbrg  3787  csbopabg  3809  pofun  4023  csbima12g  4613  csbiotag  4822  fvmpts  5175  fvmpt2  5179  mptfvex  5181  fmptcof  5256  fmptcos  5257  fliftfuns  5363  csbriotag  5404  csbov123g  5466  eqerlem  6048  qliftfuns  6101
  Copyright terms: Public domain W3C validator