Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  csbeq1 Structured version   Visualization version   GIF version

Theorem csbeq1 3832
 Description: Analogue of dfsbcq 3723 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 3723 . . 3 (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝑦𝐶[𝐵 / 𝑥]𝑦𝐶))
21abbidv 2862 . 2 (𝐴 = 𝐵 → {𝑦[𝐴 / 𝑥]𝑦𝐶} = {𝑦[𝐵 / 𝑥]𝑦𝐶})
3 df-csb 3830 . 2 𝐴 / 𝑥𝐶 = {𝑦[𝐴 / 𝑥]𝑦𝐶}
4 df-csb 3830 . 2 𝐵 / 𝑥𝐶 = {𝑦[𝐵 / 𝑥]𝑦𝐶}
52, 3, 43eqtr4g 2858 1 (𝐴 = 𝐵𝐴 / 𝑥𝐶 = 𝐵 / 𝑥𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  {cab 2776  [wsbc 3721  ⦋csb 3829 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-sbc 3722  df-csb 3830 This theorem is referenced by:  csbeq1d  3833  csbeq1a  3843  csbiebg  3861  cbvrabcsfw  3870  cbvralcsf  3871  cbvreucsf  3873  cbvrabcsf  3874  sbcnestgfw  4328  sbcnestgf  4333  csbun  4348  csbin  4349  csbif  4482  disjors  5014  disjxiun  5030  sbcbr123  5087  csbopab  5410  csbopabgALT  5411  pofun  5458  csbima12  5917  csbiota  6322  fvmpt2f  6753  fvmpts  6755  fvmpt2i  6762  fvmptex  6766  elfvmptrab1w  6778  elfvmptrab1  6779  fmptcof  6876  fmptcos  6877  fliftfuns  7053  csbriota  7115  riotaeqimp  7126  csbov123  7184  elovmporab1w  7380  elovmporab1  7381  el2mpocsbcl  7773  mposn  7791  mpocurryvald  7934  fvmpocurryd  7935  eqerlem  8321  qliftfuns  8382  boxcutc  8503  iunfi  8811  wdom2d  9043  summolem2a  15081  zsum  15084  fsum  15086  sumsnf  15108  sumsns  15114  fsum2dlem  15134  fsumcom2  15138  fsumshftm  15145  fsum0diag2  15147  fsumrlim  15175  fsumo1  15176  fsumiun  15185  prodmolem2a  15297  prodsn  15325  prodsnf  15327  fprodm1s  15333  fprodp1s  15334  prodsns  15335  fprod2dlem  15343  fprodcom2  15347  pcmptdvds  16237  gsummpt1n0  19096  telgsumfzslem  19119  telgsumfzs  19120  psrass1lemOLD  20645  psrass1lem  20648  coe1fzgsumdlem  20968  gsummoncoe1  20971  evl1gsumdlem  21018  madugsum  21286  fiuncmp  22047  elmptrab  22470  ovolfiniun  24143  finiunmbl  24186  volfiniun  24189  iundisj  24190  iundisj2  24191  iunmbl  24195  itgfsum  24468  dvfsumle  24662  dvfsumabs  24664  dvfsumlem2  24668  dvfsumlem3  24669  dvfsumlem4  24670  dvfsum2  24675  itgsubstlem  24689  itgsubst  24690  rlimcnp2  25593  fsumdvdscom  25811  fsumdvdsmul  25821  fsumvma  25838  dchrisumlem2  26115  ifeqeqx  30350  disji2f  30381  disjorsf  30384  disjif2  30385  disjabrex  30386  disjabrexf  30387  disjxpin  30392  iundisjf  30393  iundisj2f  30394  disjunsn  30398  aciunf1lem  30466  funcnv4mpt  30473  iundisjfi  30586  iundisj2fi  30587  fsumiunle  30612  gsummpt2co  30779  csbdif  34809  finixpnum  35109  poimirlem24  35148  poimirlem26  35150  csbeq12  35663  fsumshftd  36315  cdlemk54  38321  mzpsubst  39776  rabdiophlem2  39830  elnn0rabdioph  39831  dvdsrabdioph  39838  fphpd  39844  monotuz  39969  oddcomabszz  39972  fnwe2lem3  40083  flcidc  40205  csbcog  40437  sumsnd  41742  disjf1  41895  disjrnmpt2  41901  climinf2mpt  42440  climinfmpt  42441  dvnmptdivc  42664  fourierdlem103  42935  fourierdlem104  42936  csbafv12g  43777  csbaovg  43820  csbafv212g  43859  fargshiftfva  44044
 Copyright terms: Public domain W3C validator