Theorem csbeq1a 3007

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

Syntax hints:   → wi 4   = wceq 1331  ⦋csb 2998

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-sbc 2905  df-csb 2999

This theorem is referenced by:  csbhypf  3033  csbiebt  3034  sbcnestgf  3046  cbvralcsf  3057  cbvrexcsf  3058  cbvreucsf  3059  cbvrabcsf  3060  csbing  3278  disjnims  3916  disjiun  3919  sbcbrg  3977  moop2  4168  pofun  4229  eusvnf  4369  opeliunxp  4589  elrnmpt1  4785  resmptf  4864  csbima12g  4895  fvmpts  5492  fvmpt2  5497  mptfvex  5499  fmptco  5579  fmptcof  5580  fmptcos  5581  elabrex  5652  fliftfuns  5692  csbov123g  5802  ovmpos  5887  csbopeq1a  6079  mpomptsx  6088  dmmpossx  6090  fmpox  6091  mpofvex  6094  fmpoco  6106  disjxp1  6126  eqerlem  6453  qliftfuns  6506  mptelixpg  6621  xpf1o  6731  iunfidisj  6827  seq3f1olemstep  10267  seq3f1olemp  10268  sumeq2  11121  sumfct  11136  sumrbdclem  11138  summodclem3  11142  summodclem2a  11143  zsumdc  11146  fsumgcl  11148  fsum3  11149  isumss  11153  isumss2  11155  fsum3cvg2  11156  fsumzcl2  11167  fsumsplitf  11170  sumsnf  11171  sumsns  11177  fsumsplitsnun  11181  fsum2dlemstep  11196  fsumcnv  11199  fisumcom2  11200  fsumshftm  11207  fisum0diag2  11209  fsummulc2  11210  fsum00  11224  fsumabs  11227  fsumrelem  11233  fsumiun  11239  isumshft  11252  mertenslem2  11298  prodeq2  11319  prodrbdclem  11333  ctiunctlemudc  11939  ctiunctlemf  11940  iuncld  12273  fsumcncntop  12714  limcmpted  12790