Theorem csbeq1a 3090

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

Syntax hints:   → wi 4   = wceq 1364  ⦋csb 3081

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-sbc 2987  df-csb 3082

This theorem is referenced by:  csbhypf  3120  csbiebt  3121  sbcnestgf  3133  cbvralcsf  3144  cbvrexcsf  3145  cbvreucsf  3146  cbvrabcsf  3147  rspc2vd  3150  csbing  3367  disjnims  4022  disjiun  4025  sbcbrg  4084  moop2  4281  pofun  4344  eusvnf  4485  opeliunxp  4715  elrnmpt1  4914  resmptf  4993  csbima12g  5027  fvmpts  5636  fvmpt2  5642  mptfvex  5644  fmptco  5725  fmptcof  5726  fmptcos  5727  elabrex  5801  elabrexg  5802  fliftfuns  5842  csbov123g  5957  ovmpos  6043  fvmpopr2d  6056  csbopeq1a  6243  mpomptsx  6252  dmmpossx  6254  fmpox  6255  mpofvex  6260  fmpoco  6271  disjxp1  6291  eqerlem  6620  qliftfuns  6675  mptelixpg  6790  xpf1o  6902  iunfidisj  7007  cc3  7330  seq3f1olemstep  10588  seq3f1olemp  10589  sumeq2  11505  sumfct  11520  sumrbdclem  11523  summodclem3  11526  summodclem2a  11527  zsumdc  11530  fsumgcl  11532  fsum3  11533  isumss  11537  isumss2  11539  fsum3cvg2  11540  fsumzcl2  11551  fsumsplitf  11554  sumsnf  11555  sumsns  11561  fsumsplitsnun  11565  fsum2dlemstep  11580  fsumcnv  11583  fisumcom2  11584  fsumshftm  11591  fisum0diag2  11593  fsummulc2  11594  fsum00  11608  fsumabs  11611  fsumrelem  11617  fsumiun  11623  isumshft  11636  mertenslem2  11682  prodeq2  11703  prodrbdclem  11717  prodmodclem3  11721  prodmodclem2a  11722  zproddc  11725  fprodseq  11729  fprodntrivap  11730  prodfct  11733  prodssdc  11735  fprodmul  11737  prodsnf  11738  fprodm1s  11747  fprodp1s  11748  prodsns  11749  fprodcl2lem  11751  fprodcllemf  11759  fprodabs  11762  fprodap0  11767  fprod2dlemstep  11768  fprodcnv  11771  fprodcom2fi  11772  fprodrec  11775  fproddivapf  11777  fprodsplitf  11778  fprodsplit1f  11780  fprodap0f  11782  fprodle  11786  fprodmodd  11787  pcmpt  12484  pcmptdvds  12486  ctiunctlemudc  12597  ctiunctlemf  12598  ctiunctal  12601  gsumfzfsumlemm  14086  iuncld  14294  fsumcncntop  14746  limcmpted  14842  dvmptfsum  14904