Theorem csbeq1a 2977

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 2976	. 2 ⊢ ⦋𝑥 / 𝑥⦌𝐵 = 𝐵
2		csbeq1 2972	. 2 ⊢ (𝑥 = 𝐴 → ⦋𝑥 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
3	1, 2	syl5eqr 2159	1 ⊢ (𝑥 = 𝐴 → 𝐵 = ⦋𝐴 / 𝑥⦌𝐵)

Syntax hints:   → wi 4   = wceq 1312  ⦋csb 2969

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-11 1465  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-sbc 2877  df-csb 2970

This theorem is referenced by:  csbhypf  3002  csbiebt  3003  sbcnestgf  3015  cbvralcsf  3026  cbvrexcsf  3027  cbvreucsf  3028  cbvrabcsf  3029  csbing  3247  disjnims  3885  disjiun  3888  sbcbrg  3942  moop2  4131  pofun  4192  eusvnf  4332  opeliunxp  4552  elrnmpt1  4748  resmptf  4825  csbima12g  4856  fvmpts  5451  fvmpt2  5456  mptfvex  5458  fmptco  5538  fmptcof  5539  fmptcos  5540  elabrex  5611  fliftfuns  5651  csbov123g  5761  ovmpos  5846  csbopeq1a  6037  mpomptsx  6046  dmmpossx  6048  fmpox  6049  mpofvex  6052  fmpoco  6064  disjxp1  6084  eqerlem  6411  qliftfuns  6464  mptelixpg  6579  xpf1o  6688  iunfidisj  6783  seq3f1olemstep  10160  seq3f1olemp  10161  sumeq2  11013  sumfct  11028  sumrbdclem  11030  summodclem3  11034  summodclem2a  11035  zsumdc  11038  fsumgcl  11040  fsum3  11041  isumss  11045  isumss2  11047  fsum3cvg2  11048  fsumzcl2  11059  fsumsplitf  11062  sumsnf  11063  sumsns  11069  fsumsplitsnun  11073  fsum2dlemstep  11088  fsumcnv  11091  fisumcom2  11092  fsumshftm  11099  fisum0diag2  11101  fsummulc2  11102  fsum00  11116  fsumabs  11119  fsumrelem  11125  fsumiun  11131  isumshft  11144  mertenslem2  11190  ctiunctlemudc  11786  ctiunctlemf  11787  iuncld  12120  fsumcncntop  12535  limcmpted  12581