Metamath Proof Explorer


Theorem csbfv12gALTVD

Description: Virtual deduction proof of csbfv12 . The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. csbfv12 is csbfv12gALTVD without virtual deductions and was automatically derived from csbfv12gALTVD .

1:: |- (. A e. C ->. A e. C ).
2:1: |- (. A e. C ->. [_ A / x ]_ { y } = { y } ).
3:1: |- (. A e. C ->. [_ A / x ]_ ( F " { B } ) = ( [_ A / x ]_ F " [_ A / x ]_ { B } ) ).
4:1: |- (. A e. C ->. [_ A / x ]_ { B } = { [_ A / x ]_ B } ).
5:4: |- (. A e. C ->. ( [_ A / x ]_ F " [_ A / x ]_ { B } ) = ( [_ A / x ]_ F " { [_ A / x ]_ B } ) ).
6:3,5: |- (. A e. C ->. [_ A / x ]_ ( F " { B } ) = ( [_ A / x ]_ F " { [_ A / x ]_ B } ) ).
7:1: |- (. A e. C ->. ( [. A / x ]. ( F " { B } ) = { y } <-> [_ A / x ]_ ( F " { B } ) = [_ A / x ]_ { y } ) ).
8:6,2: |- (. A e. C ->. ( [_ A / x ]_ ( F " { B } ) = [_ A / x ]_ { y } <-> ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } ) ).
9:7,8: |- (. A e. C ->. ( [. A / x ]. ( F " { B } ) = { y } <-> ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } ) ).
10:9: |- (. A e. C ->. A. y ( [. A / x ]. ( F " { B } ) = { y } <-> ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } ) ).
11:10: |- (. A e. C ->. { y | [. A / x ]. ( F " { B } ) = { y } } = { y | ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } } ).
12:1: |- (. A e. C ->. [_ A / x ]_ { y | ( F " { B } ) = { y } } = { y | [. A / x ]. ( F " { B } ) = { y } } ).
13:11,12: |- (. A e. C ->. [_ A / x ]_ { y | ( F " { B } ) = { y } } = { y | ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } } ).
14:13: |- (. A e. C ->. U. [_ A / x ]_ { y | ( F " { B } ) = { y } } = U. { y | ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } } ).
15:1: |- (. A e. C ->. [_ A / x ]_ U. { y | ( F " { B } ) = { y } } = U. [_ A / x ]_ { y | ( F " { B } ) = { y } } ).
16:14,15: |- (. A e. C ->. [_ A / x ]_ U. { y | ( F " { B } ) = { y } } = U. { y | ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } } ).
17:: |- ( FB ) = U. { y | ( F " { B } ) = { y } }
18:17: |- A. x ( FB ) = U. { y | ( F " { B } ) = { y } }
19:1,18: |- (. A e. C ->. [_ A / x ]_ ( FB ) = [_ A / x ]_ U. { y | ( F " { B } ) = { y } } ).
20:16,19: |- (. A e. C ->. [_ A / x ]_ ( FB ) = U. { y | ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } } ).
21:: |- ( [_ A / x ]_ F[_ A / x ]_ B ) = U. { y | ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } }
22:20,21: |- (. A e. C ->. [_ A / x ]_ ( FB ) = ( [_ A / x ]_ F[_ A / x ]_ B ) ).
qed:22: |- ( A e. C -> [_ A / x ]_ ( FB ) = ( [_ A / x ]_ F[_ A / x ]_ B ) )
(Contributed by Alan Sare, 10-Nov-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion csbfv12gALTVD A C A / x F B = A / x F A / x B

Proof

Step Hyp Ref Expression
1 idn1 A C A C
2 sbceqg A C [˙A / x]˙ F B = y A / x F B = A / x y
3 1 2 e1a A C [˙A / x]˙ F B = y A / x F B = A / x y
4 csbima12 A / x F B = A / x F A / x B
5 4 a1i A C A / x F B = A / x F A / x B
6 1 5 e1a A C A / x F B = A / x F A / x B
7 csbsng A C A / x B = A / x B
8 1 7 e1a A C A / x B = A / x B
9 imaeq2 A / x B = A / x B A / x F A / x B = A / x F A / x B
10 8 9 e1a A C A / x F A / x B = A / x F A / x B
11 eqeq1 A / x F B = A / x F A / x B A / x F B = A / x F A / x B A / x F A / x B = A / x F A / x B
12 11 biimprd A / x F B = A / x F A / x B A / x F A / x B = A / x F A / x B A / x F B = A / x F A / x B
13 6 10 12 e11 A C A / x F B = A / x F A / x B
14 csbconstg A C A / x y = y
15 1 14 e1a A C A / x y = y
16 eqeq12 A / x F B = A / x F A / x B A / x y = y A / x F B = A / x y A / x F A / x B = y
17 16 ex A / x F B = A / x F A / x B A / x y = y A / x F B = A / x y A / x F A / x B = y
18 13 15 17 e11 A C A / x F B = A / x y A / x F A / x B = y
19 bibi1 [˙A / x]˙ F B = y A / x F B = A / x y [˙A / x]˙ F B = y A / x F A / x B = y A / x F B = A / x y A / x F A / x B = y
20 19 biimprd [˙A / x]˙ F B = y A / x F B = A / x y A / x F B = A / x y A / x F A / x B = y [˙A / x]˙ F B = y A / x F A / x B = y
21 3 18 20 e11 A C [˙A / x]˙ F B = y A / x F A / x B = y
22 21 gen11 A C y [˙A / x]˙ F B = y A / x F A / x B = y
23 abbi y [˙A / x]˙ F B = y A / x F A / x B = y y | [˙A / x]˙ F B = y = y | A / x F A / x B = y
24 23 biimpi y [˙A / x]˙ F B = y A / x F A / x B = y y | [˙A / x]˙ F B = y = y | A / x F A / x B = y
25 22 24 e1a A C y | [˙A / x]˙ F B = y = y | A / x F A / x B = y
26 csbab A / x y | F B = y = y | [˙A / x]˙ F B = y
27 26 a1i A C A / x y | F B = y = y | [˙A / x]˙ F B = y
28 1 27 e1a A C A / x y | F B = y = y | [˙A / x]˙ F B = y
29 eqeq2 y | [˙A / x]˙ F B = y = y | A / x F A / x B = y A / x y | F B = y = y | [˙A / x]˙ F B = y A / x y | F B = y = y | A / x F A / x B = y
30 29 biimpd y | [˙A / x]˙ F B = y = y | A / x F A / x B = y A / x y | F B = y = y | [˙A / x]˙ F B = y A / x y | F B = y = y | A / x F A / x B = y
31 25 28 30 e11 A C A / x y | F B = y = y | A / x F A / x B = y
32 unieq A / x y | F B = y = y | A / x F A / x B = y A / x y | F B = y = y | A / x F A / x B = y
33 31 32 e1a A C A / x y | F B = y = y | A / x F A / x B = y
34 csbuni A / x y | F B = y = A / x y | F B = y
35 34 a1i A C A / x y | F B = y = A / x y | F B = y
36 1 35 e1a A C A / x y | F B = y = A / x y | F B = y
37 eqeq2 A / x y | F B = y = y | A / x F A / x B = y A / x y | F B = y = A / x y | F B = y A / x y | F B = y = y | A / x F A / x B = y
38 37 biimpd A / x y | F B = y = y | A / x F A / x B = y A / x y | F B = y = A / x y | F B = y A / x y | F B = y = y | A / x F A / x B = y
39 33 36 38 e11 A C A / x y | F B = y = y | A / x F A / x B = y
40 dffv4 F B = y | F B = y
41 40 ax-gen x F B = y | F B = y
42 csbeq2 x F B = y | F B = y A / x F B = A / x y | F B = y
43 42 a1i A C x F B = y | F B = y A / x F B = A / x y | F B = y
44 1 41 43 e10 A C A / x F B = A / x y | F B = y
45 eqeq2 A / x y | F B = y = y | A / x F A / x B = y A / x F B = A / x y | F B = y A / x F B = y | A / x F A / x B = y
46 45 biimpd A / x y | F B = y = y | A / x F A / x B = y A / x F B = A / x y | F B = y A / x F B = y | A / x F A / x B = y
47 39 44 46 e11 A C A / x F B = y | A / x F A / x B = y
48 dffv4 A / x F A / x B = y | A / x F A / x B = y
49 eqeq2 A / x F A / x B = y | A / x F A / x B = y A / x F B = A / x F A / x B A / x F B = y | A / x F A / x B = y
50 49 biimprcd A / x F B = y | A / x F A / x B = y A / x F A / x B = y | A / x F A / x B = y A / x F B = A / x F A / x B
51 47 48 50 e10 A C A / x F B = A / x F A / x B
52 51 in1 A C A / x F B = A / x F A / x B