Theorem csbeq1a 3067

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

Assertion

Ref	Expression
csbeq1a	|- ( x = A -> B = [_ A / x ]_ B )

Proof of Theorem csbeq1a

Step	Hyp	Ref	Expression
1		csbid 3066	. 2 |- [_ x / x ]_ B = B
2		csbeq1 3061	. 2 |- ( x = A -> [_ x / x ]_ B = [_ A / x ]_ B )
3	1, 2	eqtr3id 2224	1 |- ( x = A -> B = [_ A / x ]_ B )

Syntax hints:   -> wi 4   = wceq 1353   [_csb 3058

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-sbc 2964  df-csb 3059

This theorem is referenced by:  csbhypf  3096  csbiebt  3097  sbcnestgf  3109  cbvralcsf  3120  cbvrexcsf  3121  cbvreucsf  3122  cbvrabcsf  3123  rspc2vd  3126  csbing  3343  disjnims  3996  disjiun  3999  sbcbrg  4058  moop2  4252  pofun  4313  eusvnf  4454  opeliunxp  4682  elrnmpt1  4879  resmptf  4958  csbima12g  4990  fvmpts  5595  fvmpt2  5600  mptfvex  5602  fmptco  5683  fmptcof  5684  fmptcos  5685  elabrex  5759  fliftfuns  5799  csbov123g  5913  ovmpos  5998  csbopeq1a  6189  mpomptsx  6198  dmmpossx  6200  fmpox  6201  mpofvex  6204  fmpoco  6217  disjxp1  6237  eqerlem  6566  qliftfuns  6619  mptelixpg  6734  xpf1o  6844  iunfidisj  6945  cc3  7267  seq3f1olemstep  10501  seq3f1olemp  10502  sumeq2  11367  sumfct  11382  sumrbdclem  11385  summodclem3  11388  summodclem2a  11389  zsumdc  11392  fsumgcl  11394  fsum3  11395  isumss  11399  isumss2  11401  fsum3cvg2  11402  fsumzcl2  11413  fsumsplitf  11416  sumsnf  11417  sumsns  11423  fsumsplitsnun  11427  fsum2dlemstep  11442  fsumcnv  11445  fisumcom2  11446  fsumshftm  11453  fisum0diag2  11455  fsummulc2  11456  fsum00  11470  fsumabs  11473  fsumrelem  11479  fsumiun  11485  isumshft  11498  mertenslem2  11544  prodeq2  11565  prodrbdclem  11579  prodmodclem3  11583  prodmodclem2a  11584  zproddc  11587  fprodseq  11591  fprodntrivap  11592  prodfct  11595  prodssdc  11597  fprodmul  11599  prodsnf  11600  fprodm1s  11609  fprodp1s  11610  prodsns  11611  fprodcl2lem  11613  fprodcllemf  11621  fprodabs  11624  fprodap0  11629  fprod2dlemstep  11630  fprodcnv  11633  fprodcom2fi  11634  fprodrec  11637  fproddivapf  11639  fprodsplitf  11640  fprodsplit1f  11642  fprodap0f  11644  fprodle  11648  fprodmodd  11649  pcmpt  12341  pcmptdvds  12343  ctiunctlemudc  12438  ctiunctlemf  12439  ctiunctal  12442  iuncld  13618  fsumcncntop  14059  limcmpted  14135