Theorem csbeq1a 3156

Description: Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)

Assertion

Ref	Expression
csbeq1a	⊢ (𝑥 = 𝐴 → 𝐵 = ⦋𝐴 / 𝑥⦌𝐵)

Proof of Theorem csbeq1a

Step	Hyp	Ref	Expression
1		csbid 3155	. 2 ⊢ ⦋𝑥 / 𝑥⦌𝐵 = 𝐵
2		csbeq1 3150	. 2 ⊢ (𝑥 = 𝐴 → ⦋𝑥 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
3	1, 2	eqtr3id 2285	1 ⊢ (𝑥 = 𝐴 → 𝐵 = ⦋𝐴 / 𝑥⦌𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1402  ⦋csb 3147

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-sbc 3052  df-csb 3148

This theorem is used by:  csbhypf  3186  csbiebt  3187  sbcnestgf  3199  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  rspc2vd  3216  csbing  3438  ifeqeqxdc  3687  disjnims  4121  invdisjrab  4124  disjiun  4125  sbcbrg  4186  moop2  4394  pofun  4459  eusvnf  4601  opeliunxp  4832  elrnmpt1  5035  resmptf  5116  csbima12g  5151  fvmpts  5786  fvmpt2  5792  mptfvex  5794  fmptco  5877  fmptcof  5878  fmptcos  5879  elabrex  5966  elabrexg  5967  fliftfuns  6007  riotaeqimp  6066  csbov123g  6127  ovmpos  6215  fvmpopr2d  6228  csbopeq1a  6426  mpomptsx  6437  dmmpossx  6439  fmpox  6440  mpofvex  6445  fmpoco  6456  disjxp1  6476  eqerlem  6842  qliftfuns  6897  mptelixpg  7021  xpf1o  7149  iunfidisj  7265  cc3  7641  seq3f1olemstep  10973  seq3f1olemp  10974  sumeq2  12151  sumfct  12166  sumrbdclem  12170  summodclem3  12173  summodclem2a  12174  zsumdc  12177  fsumgcl  12179  fsum3  12180  isumss  12184  isumss2  12186  fsum3cvg2  12187  fsumzcl2  12198  fsumsplitf  12201  sumsnf  12202  sumsns  12208  fsumsplitsnun  12212  fsum2dlemstep  12227  fsumcnv  12230  fisumcom2  12231  fsumshftm  12238  fisum0diag2  12240  fsummulc2  12241  fsum00  12255  fsumabs  12258  fsumrelem  12264  fsumiun  12270  isumshft  12283  mertenslem2  12329  prodeq2  12350  prodrbdclem  12364  prodmodclem3  12368  prodmodclem2a  12369  zproddc  12372  fprodseq  12376  fprodntrivap  12377  prodfct  12380  prodssdc  12382  fprodmul  12384  prodsnf  12385  fprodm1s  12394  fprodp1s  12395  prodsns  12396  fprodcl2lem  12398  fprodcllemf  12406  fprodabs  12409  fprodap0  12414  fprod2dlemstep  12415  fprodcnv  12418  fprodcom2fi  12419  fprodrec  12422  fproddivapf  12424  fprodsplitf  12425  fprodsplit1f  12427  fprodap0f  12429  fprodle  12433  fprodmodd  12434  pcmpt  13152  pcmptdvds  13154  ctiunctlemudc  13387  ctiunctlemf  13388  ctiunctal  13391  gsummptfidmadd  14252  gsummptfidmsplit  14255  gsumsnfdcmn  14258  idjusnfi  14271  gsumcom2fi  14276  gsumfsum  15033  psrass1filem  15182  iuncld  15353  fsumcncntop  15805  limcmpted  15901  dvmptfsum  15963  fsumdvdsmul  16297