Theorem csboprg 4910

Description: Move class substitution in and out of an operation. (The proof was shortened by Andrew Salmon, 22-Oct-2011.)

Assertion

Ref	Expression
csboprg	|- (A e. D -> [_A / x]_(BFC) = ([_A / x]_B[_A / x]_F[_A / x]_C))

Proof of Theorem csboprg

Step	Hyp	Ref	Expression
1		df-opr 4886	. . 3 |- (BFC) = (F` <.B, C>.)
2	1	csbeq2i 2563	. 2 |- (A e. D -> [_A / x]_(BFC) = [_A / x]_(F` <.B, C>.))
3		csbfv12g 4699	. 2 |- (A e. D -> [_A / x]_(F` <.B, C>.) = ([_A / x]_F` [_A / x]_<.B, C>.))
4		csbeq1 2542	. . . . . 6 |- (y = A -> [_y / x]_<.B, C>. = [_A / x]_<.B, C>.)
5		csbeq1 2542	. . . . . . 7 |- (y = A -> [_y / x]_B = [_A / x]_B)
6		csbeq1 2542	. . . . . . 7 |- (y = A -> [_y / x]_C = [_A / x]_C)
7	5, 6	opeq12d 3166	. . . . . 6 |- (y = A -> <.[_y / x]_B, [_y / x]_C>. = <.[_A / x]_B, [_A / x]_C>.)
8	4, 7	eqeq12d 1899	. . . . 5 |- (y = A -> ([_y / x]_<.B, C>. = <.[_y / x]_B, [_y / x]_C>. <-> [_A / x]_<.B, C>. = <.[_A / x]_B, [_A / x]_C>.))
9		visset 2295	. . . . . 6 |- y e. _V
10		ax-17 1317	. . . . . . . 8 |- (z e. y -> A.x z e. y)
11	9, 10	hbcsb1 2568	. . . . . . 7 |- (z e. [_y / x]_B -> A.x z e. [_y / x]_B)
12	9, 10	hbcsb1 2568	. . . . . . 7 |- (z e. [_y / x]_C -> A.x z e. [_y / x]_C)
13	11, 12	hbop 3168	. . . . . 6 |- (z e. <.[_y / x]_B, [_y / x]_C>. -> A.x z e. <.[_y / x]_B, [_y / x]_C>.)
14		csbeq1a 2546	. . . . . . 7 |- (x = y -> B = [_y / x]_B)
15		csbeq1a 2546	. . . . . . 7 |- (x = y -> C = [_y / x]_C)
16	14, 15	opeq12d 3166	. . . . . 6 |- (x = y -> <.B, C>. = <.[_y / x]_B, [_y / x]_C>.)
17	9, 13, 16	csbief 2576	. . . . 5 |- [_y / x]_<.B, C>. = <.[_y / x]_B, [_y / x]_C>.
18	8, 17	vtoclg 2346	. . . 4 |- (A e. D -> [_A / x]_<.B, C>. = <.[_A / x]_B, [_A / x]_C>.)
19	18	fveq2d 4685	. . 3 |- (A e. D -> ([_A / x]_F` [_A / x]_<.B, C>.) = ([_A / x]_F` <.[_A / x]_B, [_A / x]_C>.))
20		df-opr 4886	. . 3 |- ([_A / x]_B[_A / x]_F[_A / x]_C) = ([_A / x]_F` <.[_A / x]_B, [_A / x]_C>.)
21	19, 20	syl6eqr 1946	. 2 |- (A e. D -> ([_A / x]_F` [_A / x]_<.B, C>.) = ([_A / x]_B[_A / x]_F[_A / x]_C))
22	2, 3, 21	3eqtrd 1929	1 |- (A e. D -> [_A / x]_(BFC) = ([_A / x]_B[_A / x]_F[_A / x]_C))

Syntax hints:   -> wi 3   = wceq 1298   e. wcel 1300  [_csb 2540  <.cop 3046  ` cfv 3998  (class class class)co 4884

This theorem is referenced by:  csbopr12g 4912

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1302  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-rex 2110  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-xp 4000  df-cnv 4002  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fv 4014  df-opr 4886

Copyright terms: Public domain