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

Theorem csbeq1 3673
Description: Analogue of dfsbcq 3574 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 3574 . . 3 (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝑦𝐶[𝐵 / 𝑥]𝑦𝐶))
21abbidv 2875 . 2 (𝐴 = 𝐵 → {𝑦[𝐴 / 𝑥]𝑦𝐶} = {𝑦[𝐵 / 𝑥]𝑦𝐶})
3 df-csb 3671 . 2 𝐴 / 𝑥𝐶 = {𝑦[𝐴 / 𝑥]𝑦𝐶}
4 df-csb 3671 . 2 𝐵 / 𝑥𝐶 = {𝑦[𝐵 / 𝑥]𝑦𝐶}
52, 3, 43eqtr4g 2815 1 (𝐴 = 𝐵𝐴 / 𝑥𝐶 = 𝐵 / 𝑥𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1628  wcel 2135  {cab 2742  [wsbc 3572  csb 3670
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-clab 2743  df-cleq 2749  df-clel 2752  df-sbc 3573  df-csb 3671
This theorem is referenced by:  csbeq1d  3677  csbeq1a  3679  csbiebg  3693  cbvralcsf  3702  cbvreucsf  3704  cbvrabcsf  3705  sbcnestgf  4134  csbun  4148  csbin  4149  csbif  4278  disjors  4783  disjxiun  4797  sbcbr123  4854  csbopab  5154  csbopabgALT  5155  pofun  5199  csbima12  5637  csbiota  6038  fvmpt2f  6441  fvmpts  6443  fvmpt2i  6448  fvmptex  6452  elfvmptrab1  6463  fmptcof  6556  fmptcos  6557  fliftfuns  6723  csbriota  6782  riotaeqimp  6793  csbov123  6846  elovmpt2rab1  7042  el2mpt2csbcl  7414  mpt2sn  7432  mpt2curryvald  7561  fvmpt2curryd  7562  eqerlem  7941  qliftfuns  7997  boxcutc  8113  iunfi  8415  wdom2d  8646  summolem2a  14641  zsum  14644  fsum  14646  sumsnf  14668  sumsn  14670  sumsns  14674  fsum2dlem  14696  fsumcom2  14700  fsumcom2OLD  14701  fsumshftm  14708  fsum0diag2  14710  fsumrlim  14738  fsumo1  14739  fsumiun  14748  prodmolem2a  14859  prodsn  14887  prodsnf  14889  fprodm1s  14895  fprodp1s  14896  prodsns  14897  fprod2dlem  14905  fprodcom2  14909  fprodcom2OLD  14910  pcmptdvds  15796  gsummpt1n0  18560  telgsumfzslem  18581  telgsumfzs  18582  psrass1lem  19575  coe1fzgsumdlem  19869  gsummoncoe1  19872  evl1gsumdlem  19918  madugsum  20647  fiuncmp  21405  elmptrab  21828  ovolfiniun  23465  finiunmbl  23508  volfiniun  23511  iundisj  23512  iundisj2  23513  iunmbl  23517  itgfsum  23788  dvfsumle  23979  dvfsumabs  23981  dvfsumlem2  23985  dvfsumlem3  23986  dvfsumlem4  23987  dvfsum2  23992  itgsubstlem  24006  itgsubst  24007  rlimcnp2  24888  fsumdvdscom  25106  fsumdvdsmul  25116  fsumvma  25133  dchrisumlem2  25374  ifeqeqx  29664  disji2f  29693  disjorsf  29696  disjif2  29697  disjabrex  29698  disjabrexf  29699  disjxpin  29704  iundisjf  29705  iundisj2f  29706  disjunsn  29710  aciunf1lem  29767  funcnv4mpt  29775  iundisjfi  29860  iundisj2fi  29861  fsumiunle  29880  gsummpt2co  30085  csbdif  33478  finixpnum  33703  poimirlem24  33742  poimirlem26  33744  csbeq12  34275  fsumshftd  34737  cdlemk54  36744  mzpsubst  37809  rabdiophlem2  37864  elnn0rabdioph  37865  dvdsrabdioph  37872  fphpd  37878  monotuz  38004  oddcomabszz  38007  fnwe2lem3  38120  flcidc  38242  csbcog  38439  csbingOLD  39550  sumsnd  39680  disjf1  39864  disjrnmpt2  39870  climinf2mpt  40445  climinfmpt  40446  dvnmptdivc  40652  fourierdlem103  40925  fourierdlem104  40926  csbafv12g  41719  csbaovg  41762  fargshiftfva  41885
  Copyright terms: Public domain W3C validator