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

Theorem csbeq1 3012
 Description: Analog of dfsbcq 2917 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
Assertion
Ref Expression
csbeq1 (𝐴 = 𝐵𝐴 / 𝑥𝐶 = 𝐵 / 𝑥𝐶)

Proof of Theorem csbeq1
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 dfsbcq 2917 . . 3 (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝑦𝐶[𝐵 / 𝑥]𝑦𝐶))
21abbidv 2259 . 2 (𝐴 = 𝐵 → {𝑦[𝐴 / 𝑥]𝑦𝐶} = {𝑦[𝐵 / 𝑥]𝑦𝐶})
3 df-csb 3010 . 2 𝐴 / 𝑥𝐶 = {𝑦[𝐴 / 𝑥]𝑦𝐶}
4 df-csb 3010 . 2 𝐵 / 𝑥𝐶 = {𝑦[𝐵 / 𝑥]𝑦𝐶}
52, 3, 43eqtr4g 2199 1 (𝐴 = 𝐵𝐴 / 𝑥𝐶 = 𝐵 / 𝑥𝐶)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1332   ∈ wcel 1481  {cab 2127  [wsbc 2915  ⦋csb 3009 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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2123 This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1738  df-clab 2128  df-cleq 2134  df-clel 2137  df-sbc 2916  df-csb 3010 This theorem is referenced by:  csbeq1d  3016  csbeq1a  3018  csbiebg  3049  sbcnestgf  3058  cbvralcsf  3069  cbvrexcsf  3070  cbvreucsf  3071  cbvrabcsf  3072  csbing  3290  disjnims  3931  sbcbrg  3992  csbopabg  4016  pofun  4245  csbima12g  4912  csbiotag  5128  fvmpts  5511  fvmpt2  5516  mptfvex  5518  elfvmptrab1  5527  fmptcof  5599  fmptcos  5600  fliftfuns  5711  csbriotag  5754  csbov123g  5821  eqerlem  6472  qliftfuns  6525  summodclem2a  11211  zsumdc  11214  fsum3  11217  sumsnf  11239  sumsns  11245  fsum2dlemstep  11264  fisumcom2  11268  fsumshftm  11275  fisum0diag2  11277  fsumiun  11307  ctiunctlemf  12023  mulcncflem  12834
 Copyright terms: Public domain W3C validator