Theorem csbeq1a 3106

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 3105	. 2 ⊢ ⦋𝑥 / 𝑥⦌𝐵 = 𝐵
2		csbeq1 3100	. 2 ⊢ (𝑥 = 𝐴 → ⦋𝑥 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
3	1, 2	eqtr3id 2253	1 ⊢ (𝑥 = 𝐴 → 𝐵 = ⦋𝐴 / 𝑥⦌𝐵)

Syntax hints:   → wi 4   = wceq 1373  ⦋csb 3097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-sbc 3003  df-csb 3098

This theorem is referenced by:  csbhypf  3136  csbiebt  3137  sbcnestgf  3149  cbvralcsf  3160  cbvrexcsf  3161  cbvreucsf  3162  cbvrabcsf  3163  rspc2vd  3166  csbing  3384  disjnims  4042  invdisjrab  4045  disjiun  4046  sbcbrg  4106  moop2  4304  pofun  4367  eusvnf  4508  opeliunxp  4738  elrnmpt1  4938  resmptf  5018  csbima12g  5052  fvmpts  5670  fvmpt2  5676  mptfvex  5678  fmptco  5759  fmptcof  5760  fmptcos  5761  elabrex  5839  elabrexg  5840  fliftfuns  5880  csbov123g  5996  ovmpos  6082  fvmpopr2d  6095  csbopeq1a  6287  mpomptsx  6296  dmmpossx  6298  fmpox  6299  mpofvex  6304  fmpoco  6315  disjxp1  6335  eqerlem  6664  qliftfuns  6719  mptelixpg  6834  xpf1o  6956  iunfidisj  7063  cc3  7400  seq3f1olemstep  10681  seq3f1olemp  10682  sumeq2  11745  sumfct  11760  sumrbdclem  11763  summodclem3  11766  summodclem2a  11767  zsumdc  11770  fsumgcl  11772  fsum3  11773  isumss  11777  isumss2  11779  fsum3cvg2  11780  fsumzcl2  11791  fsumsplitf  11794  sumsnf  11795  sumsns  11801  fsumsplitsnun  11805  fsum2dlemstep  11820  fsumcnv  11823  fisumcom2  11824  fsumshftm  11831  fisum0diag2  11833  fsummulc2  11834  fsum00  11848  fsumabs  11851  fsumrelem  11857  fsumiun  11863  isumshft  11876  mertenslem2  11922  prodeq2  11943  prodrbdclem  11957  prodmodclem3  11961  prodmodclem2a  11962  zproddc  11965  fprodseq  11969  fprodntrivap  11970  prodfct  11973  prodssdc  11975  fprodmul  11977  prodsnf  11978  fprodm1s  11987  fprodp1s  11988  prodsns  11989  fprodcl2lem  11991  fprodcllemf  11999  fprodabs  12002  fprodap0  12007  fprod2dlemstep  12008  fprodcnv  12011  fprodcom2fi  12012  fprodrec  12015  fproddivapf  12017  fprodsplitf  12018  fprodsplit1f  12020  fprodap0f  12022  fprodle  12026  fprodmodd  12027  pcmpt  12741  pcmptdvds  12743  ctiunctlemudc  12883  ctiunctlemf  12884  ctiunctal  12887  gsumfzfsumlemm  14424  iuncld  14662  fsumcncntop  15114  limcmpted  15210  dvmptfsum  15272  fsumdvdsmul  15538