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

Theorem csbeq1 3502
Description: Analogue of dfsbcq 3404 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 3404 . . 3 (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝑦𝐶[𝐵 / 𝑥]𝑦𝐶))
21abbidv 2728 . 2 (𝐴 = 𝐵 → {𝑦[𝐴 / 𝑥]𝑦𝐶} = {𝑦[𝐵 / 𝑥]𝑦𝐶})
3 df-csb 3500 . 2 𝐴 / 𝑥𝐶 = {𝑦[𝐴 / 𝑥]𝑦𝐶}
4 df-csb 3500 . 2 𝐵 / 𝑥𝐶 = {𝑦[𝐵 / 𝑥]𝑦𝐶}
52, 3, 43eqtr4g 2669 1 (𝐴 = 𝐵𝐴 / 𝑥𝐶 = 𝐵 / 𝑥𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  wcel 1977  {cab 2596  [wsbc 3402  csb 3499
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-sbc 3403  df-csb 3500
This theorem is referenced by:  csbeq1d  3506  csbeq1a  3508  csbiebg  3522  cbvralcsf  3531  cbvreucsf  3533  cbvrabcsf  3534  sbcnestgf  3947  csbun  3961  csbin  3962  csbif  4088  disjors  4568  disjxiun  4579  disjxiunOLD  4580  sbcbr123  4636  csbopab  4932  csbopabgALT  4933  pofun  4975  csbima12  5402  csbiota  5797  fvmpt2f  6192  fvmpts  6194  fvmpt2i  6199  fvmptex  6203  elfvmptrab1  6213  fmptcof  6304  fmptcos  6305  fliftfuns  6464  csbriota  6523  csbov123  6585  elovmpt2rab1  6779  el2mpt2csbcl  7137  mpt2sn  7155  mpt2curryvald  7283  fvmpt2curryd  7284  eqerlem  7663  qliftfuns  7721  boxcutc  7837  iunfi  8137  wdom2d  8368  summolem2a  14293  zsum  14296  fsum  14298  sumsn  14319  sumsns  14323  fsum2dlem  14343  fsumcom2  14347  fsumcom2OLD  14348  fsumshftm  14355  fsum0diag2  14357  fsumrlim  14384  fsumo1  14385  fsumiun  14394  prodmolem2a  14503  prodsn  14531  prodsnf  14533  fprodm1s  14539  fprodp1s  14540  prodsns  14541  fprod2dlem  14549  fprodcom2  14553  fprodcom2OLD  14554  pcmptdvds  15436  gsummpt1n0  18187  telgsumfzslem  18208  telgsumfzs  18209  psrass1lem  19198  coe1fzgsumdlem  19492  gsummoncoe1  19495  evl1gsumdlem  19541  madugsum  20268  fiuncmp  21017  elmptrab  21440  ovolfiniun  23076  finiunmbl  23119  volfiniun  23122  iundisj  23123  iundisj2  23124  iunmbl  23128  itgfsum  23399  dvfsumle  23588  dvfsumabs  23590  dvfsumlem2  23594  dvfsumlem3  23595  dvfsumlem4  23596  dvfsum2  23601  itgsubstlem  23615  itgsubst  23616  rlimcnp2  24493  fsumdvdscom  24711  fsumdvdsmul  24721  fsumvma  24738  dchrisumlem2  24979  fargshiftfva  26167  ifeqeqx  28745  disji2f  28772  disjorsf  28775  disjif2  28776  disjabrex  28777  disjabrexf  28778  disjxpin  28783  iundisjf  28784  iundisj2f  28785  disjunsn  28789  aciunf1lem  28844  funcnv4mpt  28853  iundisjfi  28942  iundisj2fi  28943  gsummpt2co  29111  csbdif  32347  finixpnum  32564  poimirlem24  32603  poimirlem26  32605  csbeq12  33136  fsumshftd  33255  fsumshftdOLD  33256  cdlemk54  35264  mzpsubst  36329  rabdiophlem2  36384  elnn0rabdioph  36385  dvdsrabdioph  36392  fphpd  36398  monotuz  36524  oddcomabszz  36527  fnwe2lem3  36640  flcidc  36763  csbcog  36960  csbingOLD  38076  sumsnd  38208  disjf1  38364  disjrnmpt2  38370  sumsnf  38636  dvnmptdivc  38828  fourierdlem103  39102  fourierdlem104  39103  csbafv12g  39866  csbaovg  39909  riotaeqimp  40338
  Copyright terms: Public domain W3C validator