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

Theorem csbeq1 3731
Description: Analogue of dfsbcq 3635 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 3635 . . 3 (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝑦𝐶[𝐵 / 𝑥]𝑦𝐶))
21abbidv 2925 . 2 (𝐴 = 𝐵 → {𝑦[𝐴 / 𝑥]𝑦𝐶} = {𝑦[𝐵 / 𝑥]𝑦𝐶})
3 df-csb 3729 . 2 𝐴 / 𝑥𝐶 = {𝑦[𝐴 / 𝑥]𝑦𝐶}
4 df-csb 3729 . 2 𝐵 / 𝑥𝐶 = {𝑦[𝐵 / 𝑥]𝑦𝐶}
52, 3, 43eqtr4g 2865 1 (𝐴 = 𝐵𝐴 / 𝑥𝐶 = 𝐵 / 𝑥𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wcel 2156  {cab 2792  [wsbc 3633  csb 3728
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-sbc 3634  df-csb 3729
This theorem is referenced by:  csbeq1d  3735  csbeq1a  3737  csbiebg  3751  cbvralcsf  3760  cbvreucsf  3762  cbvrabcsf  3763  sbcnestgf  4192  csbun  4207  csbin  4208  csbif  4334  disjors  4827  disjxiun  4841  sbcbr123  4898  csbopab  5203  csbopabgALT  5204  pofun  5248  csbima12  5693  csbiota  6094  fvmpt2f  6504  fvmpts  6506  fvmpt2i  6511  fvmptex  6515  elfvmptrab1  6526  fmptcof  6620  fmptcos  6621  fliftfuns  6788  csbriota  6847  riotaeqimp  6858  csbov123  6915  elovmpt2rab1  7111  el2mpt2csbcl  7483  mpt2sn  7502  mpt2curryvald  7631  fvmpt2curryd  7632  eqerlem  8013  qliftfuns  8069  boxcutc  8188  iunfi  8493  wdom2d  8724  summolem2a  14669  zsum  14672  fsum  14674  sumsnf  14696  sumsn  14698  sumsns  14702  fsum2dlem  14724  fsumcom2  14728  fsumshftm  14735  fsum0diag2  14737  fsumrlim  14765  fsumo1  14766  fsumiun  14775  prodmolem2a  14885  prodsn  14913  prodsnf  14915  fprodm1s  14921  fprodp1s  14922  prodsns  14923  fprod2dlem  14931  fprodcom2  14935  pcmptdvds  15815  gsummpt1n0  18565  telgsumfzslem  18587  telgsumfzs  18588  psrass1lem  19586  coe1fzgsumdlem  19879  gsummoncoe1  19882  evl1gsumdlem  19928  madugsum  20660  fiuncmp  21421  elmptrab  21844  ovolfiniun  23482  finiunmbl  23525  volfiniun  23528  iundisj  23529  iundisj2  23530  iunmbl  23534  itgfsum  23807  dvfsumle  23998  dvfsumabs  24000  dvfsumlem2  24004  dvfsumlem3  24005  dvfsumlem4  24006  dvfsum2  24011  itgsubstlem  24025  itgsubst  24026  rlimcnp2  24907  fsumdvdscom  25125  fsumdvdsmul  25135  fsumvma  25152  dchrisumlem2  25393  ifeqeqx  29686  disji2f  29715  disjorsf  29718  disjif2  29719  disjabrex  29720  disjabrexf  29721  disjxpin  29726  iundisjf  29727  iundisj2f  29728  disjunsn  29732  aciunf1lem  29789  funcnv4mpt  29797  iundisjfi  29882  iundisj2fi  29883  fsumiunle  29902  gsummpt2co  30105  csbdif  33488  finixpnum  33707  poimirlem24  33746  poimirlem26  33748  csbeq12  34276  fsumshftd  34731  cdlemk54  36739  mzpsubst  37813  rabdiophlem2  37868  elnn0rabdioph  37869  dvdsrabdioph  37876  fphpd  37882  monotuz  38007  oddcomabszz  38010  fnwe2lem3  38123  flcidc  38245  csbcog  38441  csbingOLD  39549  sumsnd  39679  disjf1  39858  disjrnmpt2  39864  climinf2mpt  40426  climinfmpt  40427  dvnmptdivc  40633  fourierdlem103  40905  fourierdlem104  40906  csbafv12g  41726  csbaovg  41769  csbafv212g  41808  fargshiftfva  41954
  Copyright terms: Public domain W3C validator