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

Theorem csbeq1 3522
Description: Analogue of dfsbcq 3424 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 3424 . . 3 (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝑦𝐶[𝐵 / 𝑥]𝑦𝐶))
21abbidv 2738 . 2 (𝐴 = 𝐵 → {𝑦[𝐴 / 𝑥]𝑦𝐶} = {𝑦[𝐵 / 𝑥]𝑦𝐶})
3 df-csb 3520 . 2 𝐴 / 𝑥𝐶 = {𝑦[𝐴 / 𝑥]𝑦𝐶}
4 df-csb 3520 . 2 𝐵 / 𝑥𝐶 = {𝑦[𝐵 / 𝑥]𝑦𝐶}
52, 3, 43eqtr4g 2680 1 (𝐴 = 𝐵𝐴 / 𝑥𝐶 = 𝐵 / 𝑥𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wcel 1987  {cab 2607  [wsbc 3422  csb 3519
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-sbc 3423  df-csb 3520
This theorem is referenced by:  csbeq1d  3526  csbeq1a  3528  csbiebg  3542  cbvralcsf  3551  cbvreucsf  3553  cbvrabcsf  3554  sbcnestgf  3973  csbun  3987  csbin  3988  csbif  4116  disjors  4608  disjxiun  4619  disjxiunOLD  4620  sbcbr123  4676  csbopab  4978  csbopabgALT  4979  pofun  5021  csbima12  5452  csbiota  5850  fvmpt2f  6250  fvmpts  6252  fvmpt2i  6257  fvmptex  6261  elfvmptrab1  6271  fmptcof  6363  fmptcos  6364  fliftfuns  6529  csbriota  6588  riotaeqimp  6599  csbov123  6652  elovmpt2rab1  6846  el2mpt2csbcl  7210  mpt2sn  7228  mpt2curryvald  7356  fvmpt2curryd  7357  eqerlem  7736  qliftfuns  7794  boxcutc  7911  iunfi  8214  wdom2d  8445  summolem2a  14395  zsum  14398  fsum  14400  sumsnf  14422  sumsn  14424  sumsns  14428  fsum2dlem  14448  fsumcom2  14452  fsumcom2OLD  14453  fsumshftm  14460  fsum0diag2  14462  fsumrlim  14489  fsumo1  14490  fsumiun  14499  prodmolem2a  14608  prodsn  14636  prodsnf  14638  fprodm1s  14644  fprodp1s  14645  prodsns  14646  fprod2dlem  14654  fprodcom2  14658  fprodcom2OLD  14659  pcmptdvds  15541  gsummpt1n0  18304  telgsumfzslem  18325  telgsumfzs  18326  psrass1lem  19317  coe1fzgsumdlem  19611  gsummoncoe1  19614  evl1gsumdlem  19660  madugsum  20389  fiuncmp  21147  elmptrab  21570  ovolfiniun  23209  finiunmbl  23252  volfiniun  23255  iundisj  23256  iundisj2  23257  iunmbl  23261  itgfsum  23533  dvfsumle  23722  dvfsumabs  23724  dvfsumlem2  23728  dvfsumlem3  23729  dvfsumlem4  23730  dvfsum2  23735  itgsubstlem  23749  itgsubst  23750  rlimcnp2  24627  fsumdvdscom  24845  fsumdvdsmul  24855  fsumvma  24872  dchrisumlem2  25113  ifeqeqx  29249  disji2f  29276  disjorsf  29279  disjif2  29280  disjabrex  29281  disjabrexf  29282  disjxpin  29287  iundisjf  29288  iundisj2f  29289  disjunsn  29293  aciunf1lem  29345  funcnv4mpt  29354  iundisjfi  29438  iundisj2fi  29439  gsummpt2co  29607  csbdif  32842  finixpnum  33065  poimirlem24  33104  poimirlem26  33106  csbeq12  33637  fsumshftd  33756  fsumshftdOLD  33757  cdlemk54  35765  mzpsubst  36830  rabdiophlem2  36885  elnn0rabdioph  36886  dvdsrabdioph  36893  fphpd  36899  monotuz  37025  oddcomabszz  37028  fnwe2lem3  37141  flcidc  37264  csbcog  37461  csbingOLD  38576  sumsnd  38707  disjf1  38878  disjrnmpt2  38884  climinf2mpt  39382  climinfmpt  39383  dvnmptdivc  39490  fourierdlem103  39763  fourierdlem104  39764  csbafv12g  40551  csbaovg  40594  fargshiftfva  40707
  Copyright terms: Public domain W3C validator