Metamath Proof Explorer

Theorem csbunigVD

Description: Virtual deduction proof of csbuni . 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. csbuni is csbunigVD without virtual deductions and was automatically derived from csbunigVD .

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

Ref Expression
Assertion csbunigVD 
|- ( A e. V -> [_ A / x ]_ U. B = U. [_ A / x ]_ B )

Proof

Step Hyp Ref Expression
1 idn1 
 |-  (. A e. V ->. A e. V ).
2 sbcg 
 |-  ( A e. V -> ( [. A / x ]. z e. y <-> z e. y ) )
3 1 2 e1a 
 |-  (. A e. V ->. ( [. A / x ]. z e. y <-> z e. y ) ).
4 sbcel2 
 |-  ( [. A / x ]. y e. B <-> y e. [_ A / x ]_ B )
5 4 a1i 
 |-  ( A e. V -> ( [. A / x ]. y e. B <-> y e. [_ A / x ]_ B ) )
6 1 5 e1a 
 |-  (. A e. V ->. ( [. A / x ]. y e. B <-> y e. [_ A / x ]_ B ) ).
7 pm4.38 
 |-  ( ( ( [. A / x ]. z e. y <-> z e. y ) /\ ( [. A / x ]. y e. B <-> y e. [_ A / x ]_ B ) ) -> ( ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) )
8 7 ex 
 |-  ( ( [. A / x ]. z e. y <-> z e. y ) -> ( ( [. A / x ]. y e. B <-> y e. [_ A / x ]_ B ) -> ( ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) ) )
9 3 6 8 e11 
 |-  (. A e. V ->. ( ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) ).
10 sbcan 
 |-  ( [. A / x ]. ( z e. y /\ y e. B ) <-> ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) )
11 10 a1i 
 |-  ( A e. V -> ( [. A / x ]. ( z e. y /\ y e. B ) <-> ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) ) )
12 1 11 e1a 
 |-  (. A e. V ->. ( [. A / x ]. ( z e. y /\ y e. B ) <-> ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) ) ).
13 bibi1 
 |-  ( ( [. A / x ]. ( z e. y /\ y e. B ) <-> ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) ) -> ( ( [. A / x ]. ( z e. y /\ y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) <-> ( ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) ) )
14 13 biimprcd 
 |-  ( ( ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) -> ( ( [. A / x ]. ( z e. y /\ y e. B ) <-> ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) ) -> ( [. A / x ]. ( z e. y /\ y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) ) )
15 9 12 14 e11 
 |-  (. A e. V ->. ( [. A / x ]. ( z e. y /\ y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) ).
16 15 gen11 
 |-  (. A e. V ->. A. y ( [. A / x ]. ( z e. y /\ y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) ).
17 exbi 
 |-  ( A. y ( [. A / x ]. ( z e. y /\ y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) -> ( E. y [. A / x ]. ( z e. y /\ y e. B ) <-> E. y ( z e. y /\ y e. [_ A / x ]_ B ) ) )
18 16 17 e1a 
 |-  (. A e. V ->. ( E. y [. A / x ]. ( z e. y /\ y e. B ) <-> E. y ( z e. y /\ y e. [_ A / x ]_ B ) ) ).
19 sbcex2 
 |-  ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y [. A / x ]. ( z e. y /\ y e. B ) )
20 19 a1i 
 |-  ( A e. V -> ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y [. A / x ]. ( z e. y /\ y e. B ) ) )
21 1 20 e1a 
 |-  (. A e. V ->. ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y [. A / x ]. ( z e. y /\ y e. B ) ) ).
22 bibi1 
 |-  ( ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y [. A / x ]. ( z e. y /\ y e. B ) ) -> ( ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y ( z e. y /\ y e. [_ A / x ]_ B ) ) <-> ( E. y [. A / x ]. ( z e. y /\ y e. B ) <-> E. y ( z e. y /\ y e. [_ A / x ]_ B ) ) ) )
23 22 biimprcd 
 |-  ( ( E. y [. A / x ]. ( z e. y /\ y e. B ) <-> E. y ( z e. y /\ y e. [_ A / x ]_ B ) ) -> ( ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y [. A / x ]. ( z e. y /\ y e. B ) ) -> ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y ( z e. y /\ y e. [_ A / x ]_ B ) ) ) )
24 18 21 23 e11 
 |-  (. A e. V ->. ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y ( z e. y /\ y e. [_ A / x ]_ B ) ) ).
25 24 gen11 
 |-  (. A e. V ->. A. z ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y ( z e. y /\ y e. [_ A / x ]_ B ) ) ).
26 abbi 
 |-  ( A. z ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y ( z e. y /\ y e. [_ A / x ]_ B ) ) <-> { z | [. A / x ]. E. y ( z e. y /\ y e. B ) } = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } )
27 26 biimpi 
 |-  ( A. z ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y ( z e. y /\ y e. [_ A / x ]_ B ) ) -> { z | [. A / x ]. E. y ( z e. y /\ y e. B ) } = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } )
28 25 27 e1a 
 |-  (. A e. V ->. { z | [. A / x ]. E. y ( z e. y /\ y e. B ) } = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } ).
29 csbab 
 |-  [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } = { z | [. A / x ]. E. y ( z e. y /\ y e. B ) }
30 29 a1i 
 |-  ( A e. V -> [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } = { z | [. A / x ]. E. y ( z e. y /\ y e. B ) } )
31 1 30 e1a 
 |-  (. A e. V ->. [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } = { z | [. A / x ]. E. y ( z e. y /\ y e. B ) } ).
32 eqeq2 
 |-  ( { z | [. A / x ]. E. y ( z e. y /\ y e. B ) } = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } -> ( [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } = { z | [. A / x ]. E. y ( z e. y /\ y e. B ) } <-> [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } ) )
33 32 biimpd 
 |-  ( { z | [. A / x ]. E. y ( z e. y /\ y e. B ) } = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } -> ( [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } = { z | [. A / x ]. E. y ( z e. y /\ y e. B ) } -> [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } ) )
34 28 31 33 e11 
 |-  (. A e. V ->. [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } ).
35 df-uni 
 |-  U. B = { z | E. y ( z e. y /\ y e. B ) }
36 35 ax-gen 
 |-  A. x U. B = { z | E. y ( z e. y /\ y e. B ) }
37 spsbc 
 |-  ( A e. V -> ( A. x U. B = { z | E. y ( z e. y /\ y e. B ) } -> [. A / x ]. U. B = { z | E. y ( z e. y /\ y e. B ) } ) )
38 1 36 37 e10 
 |-  (. A e. V ->. [. A / x ]. U. B = { z | E. y ( z e. y /\ y e. B ) } ).
39 sbceqg 
 |-  ( A e. V -> ( [. A / x ]. U. B = { z | E. y ( z e. y /\ y e. B ) } <-> [_ A / x ]_ U. B = [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } ) )
40 39 biimpd 
 |-  ( A e. V -> ( [. A / x ]. U. B = { z | E. y ( z e. y /\ y e. B ) } -> [_ A / x ]_ U. B = [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } ) )
41 1 38 40 e11 
 |-  (. A e. V ->. [_ A / x ]_ U. B = [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } ).
42 eqeq2 
 |-  ( [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } -> ( [_ A / x ]_ U. B = [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } <-> [_ A / x ]_ U. B = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } ) )
43 42 biimpd 
 |-  ( [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } -> ( [_ A / x ]_ U. B = [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } -> [_ A / x ]_ U. B = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } ) )
44 34 41 43 e11 
 |-  (. A e. V ->. [_ A / x ]_ U. B = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } ).
45 df-uni 
 |-  U. [_ A / x ]_ B = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) }
46 eqeq2 
 |-  ( U. [_ A / x ]_ B = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } -> ( [_ A / x ]_ U. B = U. [_ A / x ]_ B <-> [_ A / x ]_ U. B = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } ) )
47 46 biimprcd 
 |-  ( [_ A / x ]_ U. B = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } -> ( U. [_ A / x ]_ B = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } -> [_ A / x ]_ U. B = U. [_ A / x ]_ B ) )
48 44 45 47 e10 
 |-  (. A e. V ->. [_ A / x ]_ U. B = U. [_ A / x ]_ B ).
49 48 in1 
 |-  ( A e. V -> [_ A / x ]_ U. B = U. [_ A / x ]_ B )