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

Theorem csbeq1 3498
Description: Analogue of dfsbcq 3400 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 3400 . . 3 (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝑦𝐶[𝐵 / 𝑥]𝑦𝐶))
21abbidv 2724 . 2 (𝐴 = 𝐵 → {𝑦[𝐴 / 𝑥]𝑦𝐶} = {𝑦[𝐵 / 𝑥]𝑦𝐶})
3 df-csb 3496 . 2 𝐴 / 𝑥𝐶 = {𝑦[𝐴 / 𝑥]𝑦𝐶}
4 df-csb 3496 . 2 𝐵 / 𝑥𝐶 = {𝑦[𝐵 / 𝑥]𝑦𝐶}
52, 3, 43eqtr4g 2665 1 (𝐴 = 𝐵𝐴 / 𝑥𝐶 = 𝐵 / 𝑥𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1976  {cab 2592  [wsbc 3398  csb 3495
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-sbc 3399  df-csb 3496
This theorem is referenced by:  csbeq1d  3502  csbeq1a  3504  csbiebg  3518  cbvralcsf  3527  cbvreucsf  3529  cbvrabcsf  3530  sbcnestgf  3943  csbun  3957  csbin  3958  csbif  4084  disjors  4559  disjxiun  4570  disjxiunOLD  4571  sbcbr123  4627  csbopab  4919  csbopabgALT  4920  pofun  4962  csbima12  5386  csbiota  5780  fvmpt2f  6174  fvmpts  6176  fvmpt2i  6181  fvmptex  6185  elfvmptrab1  6195  fmptcof  6286  fmptcos  6287  fliftfuns  6439  csbriota  6498  csbov123  6560  elovmpt2rab1  6753  el2mpt2csbcl  7111  mpt2sn  7129  mpt2curryvald  7257  fvmpt2curryd  7258  eqerlem  7637  qliftfuns  7695  boxcutc  7811  iunfi  8111  wdom2d  8342  summolem2a  14236  zsum  14239  fsum  14241  sumsn  14262  sumsns  14266  fsum2dlem  14286  fsumcom2  14290  fsumcom2OLD  14291  fsumshftm  14298  fsum0diag2  14300  fsumrlim  14327  fsumo1  14328  fsumiun  14337  prodmolem2a  14446  prodsn  14474  prodsnf  14476  fprodm1s  14482  fprodp1s  14483  prodsns  14484  fprod2dlem  14492  fprodcom2  14496  fprodcom2OLD  14497  pcmptdvds  15379  gsummpt1n0  18130  telgsumfzslem  18151  telgsumfzs  18152  psrass1lem  19141  coe1fzgsumdlem  19435  gsummoncoe1  19438  evl1gsumdlem  19484  madugsum  20207  fiuncmp  20956  elmptrab  21379  ovolfiniun  22990  finiunmbl  23033  volfiniun  23036  iundisj  23037  iundisj2  23038  iunmbl  23042  itgfsum  23313  dvfsumle  23502  dvfsumabs  23504  dvfsumlem2  23508  dvfsumlem3  23509  dvfsumlem4  23510  dvfsum2  23515  itgsubstlem  23529  itgsubst  23530  rlimcnp2  24407  fsumdvdscom  24625  fsumdvdsmul  24635  fsumvma  24652  dchrisumlem2  24893  fargshiftfva  25930  ifeqeqx  28548  disji2f  28575  disjorsf  28578  disjif2  28579  disjabrex  28580  disjabrexf  28581  disjxpin  28586  iundisjf  28587  iundisj2f  28588  disjunsn  28592  aciunf1lem  28647  funcnv4mpt  28656  iundisjfi  28745  iundisj2fi  28746  gsummpt2co  28914  csbdif  32147  finixpnum  32364  poimirlem24  32403  poimirlem26  32405  csbeq12  32936  fsumshftd  33055  fsumshftdOLD  33056  cdlemk54  35064  mzpsubst  36129  rabdiophlem2  36184  elnn0rabdioph  36185  dvdsrabdioph  36192  fphpd  36198  monotuz  36324  oddcomabszz  36327  fnwe2lem3  36440  flcidc  36563  csbcog  36760  csbingOLD  37876  sumsnd  38008  disjf1  38164  disjrnmpt2  38170  sumsnf  38437  dvnmptdivc  38629  fourierdlem103  38903  fourierdlem104  38904  csbafv12g  39668  csbaovg  39711  riotaeqimp  40162
  Copyright terms: Public domain W3C validator