Metamath Proof Explorer

Theorem csbingVD

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

1:: |- (. A e. B ->. A e. B ).
2:: |- ( C i^i D ) = { y | ( y e. C /\ y e. D ) }
20:2: |- A. x ( C i^i D ) = { y | ( y e. C /\ y e. D ) }
30:1,20: |- (. A e. B ->. [. A / x ]. ( C i^i D ) = { y | ( y e. C /\ y e. D ) } ).
3:1,30: |- (. A e. B ->. [_ A / x ]_ ( C i^i D ) = [_ A / x ]_ { y | ( y e. C /\ y e. D ) } ).
4:1: |- (. A e. B ->. [_ A / x ]_ { y | ( y e. C /\ y e. D ) } = { y | [. A / x ]. ( y e. C /\ y e. D ) } ).
5:3,4: |- (. A e. B ->. [_ A / x ]_ ( C i^i D ) = { y | [. A / x ]. ( y e. C /\ y e. D ) } ).
6:1: |- (. A e. B ->. ( [. A / x ]. y e. C <-> y e. [_ A / x ]_ C ) ).
7:1: |- (. A e. B ->. ( [. A / x ]. y e. D <-> y e. [_ A / x ]_ D ) ).
8:6,7: |- (. A e. B ->. ( ( [. A / x ]. y e. C /\ [. A / x ]. y e. D ) <-> ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) ) ).
9:1: |- (. A e. B ->. ( [. A / x ]. ( y e. C /\ y e. D ) <-> ( [. A / x ]. y e. C /\ [. A / x ]. y e. D ) ) ).
10:9,8: |- (. A e. B ->. ( [. A / x ]. ( y e. C /\ y e. D ) <-> ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) ) ).
11:10: |- (. A e. B ->. A. y ( [. A / x ]. ( y e. C /\ y e. D ) <-> ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) ) ).
12:11: |- (. A e. B ->. { y | [. A / x ]. ( y e. C /\ y e. D ) } = { y | ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) } ).
13:5,12: |- (. A e. B ->. [_ A / x ]_ ( C i^i D ) = { y | ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) } ).
14:: |- ( [_ A / x ]_ C i^i [_ A / x ]_ D ) = { y | ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) }
15:13,14: |- (. A e. B ->. [_ A / x ]_ ( C i^i D ) = ( [_ A / x ]_ C i^i [_ A / x ]_ D ) ).
qed:15: |- ( A e. B -> [_ A / x ]_ ( C i^i D ) = ( [_ A / x ]_ C i^i [_ A / x ]_ D ) )
(Contributed by Alan Sare, 22-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion csbingVD 
|- ( A e. B -> [_ A / x ]_ ( C i^i D ) = ( [_ A / x ]_ C i^i [_ A / x ]_ D ) )

Proof

Step Hyp Ref Expression
1 idn1 
 |-  (. A e. B ->. A e. B ).
2 df-in 
 |-  ( C i^i D ) = { y | ( y e. C /\ y e. D ) }
3 2 ax-gen 
 |-  A. x ( C i^i D ) = { y | ( y e. C /\ y e. D ) }
4 spsbc 
 |-  ( A e. B -> ( A. x ( C i^i D ) = { y | ( y e. C /\ y e. D ) } -> [. A / x ]. ( C i^i D ) = { y | ( y e. C /\ y e. D ) } ) )
5 1 3 4 e10 
 |-  (. A e. B ->. [. A / x ]. ( C i^i D ) = { y | ( y e. C /\ y e. D ) } ).
6 sbceqg 
 |-  ( A e. B -> ( [. A / x ]. ( C i^i D ) = { y | ( y e. C /\ y e. D ) } <-> [_ A / x ]_ ( C i^i D ) = [_ A / x ]_ { y | ( y e. C /\ y e. D ) } ) )
7 6 biimpd 
 |-  ( A e. B -> ( [. A / x ]. ( C i^i D ) = { y | ( y e. C /\ y e. D ) } -> [_ A / x ]_ ( C i^i D ) = [_ A / x ]_ { y | ( y e. C /\ y e. D ) } ) )
8 1 5 7 e11 
 |-  (. A e. B ->. [_ A / x ]_ ( C i^i D ) = [_ A / x ]_ { y | ( y e. C /\ y e. D ) } ).
9 csbab 
 |-  [_ A / x ]_ { y | ( y e. C /\ y e. D ) } = { y | [. A / x ]. ( y e. C /\ y e. D ) }
10 9 a1i 
 |-  ( A e. B -> [_ A / x ]_ { y | ( y e. C /\ y e. D ) } = { y | [. A / x ]. ( y e. C /\ y e. D ) } )
11 1 10 e1a 
 |-  (. A e. B ->. [_ A / x ]_ { y | ( y e. C /\ y e. D ) } = { y | [. A / x ]. ( y e. C /\ y e. D ) } ).
12 eqeq1 
 |-  ( [_ A / x ]_ ( C i^i D ) = [_ A / x ]_ { y | ( y e. C /\ y e. D ) } -> ( [_ A / x ]_ ( C i^i D ) = { y | [. A / x ]. ( y e. C /\ y e. D ) } <-> [_ A / x ]_ { y | ( y e. C /\ y e. D ) } = { y | [. A / x ]. ( y e. C /\ y e. D ) } ) )
13 12 biimprd 
 |-  ( [_ A / x ]_ ( C i^i D ) = [_ A / x ]_ { y | ( y e. C /\ y e. D ) } -> ( [_ A / x ]_ { y | ( y e. C /\ y e. D ) } = { y | [. A / x ]. ( y e. C /\ y e. D ) } -> [_ A / x ]_ ( C i^i D ) = { y | [. A / x ]. ( y e. C /\ y e. D ) } ) )
14 8 11 13 e11 
 |-  (. A e. B ->. [_ A / x ]_ ( C i^i D ) = { y | [. A / x ]. ( y e. C /\ y e. D ) } ).
15 sbcan 
 |-  ( [. A / x ]. ( y e. C /\ y e. D ) <-> ( [. A / x ]. y e. C /\ [. A / x ]. y e. D ) )
16 15 a1i 
 |-  ( A e. B -> ( [. A / x ]. ( y e. C /\ y e. D ) <-> ( [. A / x ]. y e. C /\ [. A / x ]. y e. D ) ) )
17 1 16 e1a 
 |-  (. A e. B ->. ( [. A / x ]. ( y e. C /\ y e. D ) <-> ( [. A / x ]. y e. C /\ [. A / x ]. y e. D ) ) ).
18 sbcel2 
 |-  ( [. A / x ]. y e. C <-> y e. [_ A / x ]_ C )
19 18 a1i 
 |-  ( A e. B -> ( [. A / x ]. y e. C <-> y e. [_ A / x ]_ C ) )
20 1 19 e1a 
 |-  (. A e. B ->. ( [. A / x ]. y e. C <-> y e. [_ A / x ]_ C ) ).
21 sbcel2 
 |-  ( [. A / x ]. y e. D <-> y e. [_ A / x ]_ D )
22 21 a1i 
 |-  ( A e. B -> ( [. A / x ]. y e. D <-> y e. [_ A / x ]_ D ) )
23 1 22 e1a 
 |-  (. A e. B ->. ( [. A / x ]. y e. D <-> y e. [_ A / x ]_ D ) ).
24 pm4.38 
 |-  ( ( ( [. A / x ]. y e. C <-> y e. [_ A / x ]_ C ) /\ ( [. A / x ]. y e. D <-> y e. [_ A / x ]_ D ) ) -> ( ( [. A / x ]. y e. C /\ [. A / x ]. y e. D ) <-> ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) ) )
25 24 ex 
 |-  ( ( [. A / x ]. y e. C <-> y e. [_ A / x ]_ C ) -> ( ( [. A / x ]. y e. D <-> y e. [_ A / x ]_ D ) -> ( ( [. A / x ]. y e. C /\ [. A / x ]. y e. D ) <-> ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) ) ) )
26 20 23 25 e11 
 |-  (. A e. B ->. ( ( [. A / x ]. y e. C /\ [. A / x ]. y e. D ) <-> ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) ) ).
27 bibi1 
 |-  ( ( [. A / x ]. ( y e. C /\ y e. D ) <-> ( [. A / x ]. y e. C /\ [. A / x ]. y e. D ) ) -> ( ( [. A / x ]. ( y e. C /\ y e. D ) <-> ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) ) <-> ( ( [. A / x ]. y e. C /\ [. A / x ]. y e. D ) <-> ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) ) ) )
28 27 biimprd 
 |-  ( ( [. A / x ]. ( y e. C /\ y e. D ) <-> ( [. A / x ]. y e. C /\ [. A / x ]. y e. D ) ) -> ( ( ( [. A / x ]. y e. C /\ [. A / x ]. y e. D ) <-> ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) ) -> ( [. A / x ]. ( y e. C /\ y e. D ) <-> ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) ) ) )
29 17 26 28 e11 
 |-  (. A e. B ->. ( [. A / x ]. ( y e. C /\ y e. D ) <-> ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) ) ).
30 29 gen11 
 |-  (. A e. B ->. A. y ( [. A / x ]. ( y e. C /\ y e. D ) <-> ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) ) ).
31 abbib 
 |-  ( { y | [. A / x ]. ( y e. C /\ y e. D ) } = { y | ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) } <-> A. y ( [. A / x ]. ( y e. C /\ y e. D ) <-> ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) ) )
32 31 biimpri 
 |-  ( A. y ( [. A / x ]. ( y e. C /\ y e. D ) <-> ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) ) -> { y | [. A / x ]. ( y e. C /\ y e. D ) } = { y | ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) } )
33 30 32 e1a 
 |-  (. A e. B ->. { y | [. A / x ]. ( y e. C /\ y e. D ) } = { y | ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) } ).
34 eqeq1 
 |-  ( [_ A / x ]_ ( C i^i D ) = { y | [. A / x ]. ( y e. C /\ y e. D ) } -> ( [_ A / x ]_ ( C i^i D ) = { y | ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) } <-> { y | [. A / x ]. ( y e. C /\ y e. D ) } = { y | ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) } ) )
35 34 biimprd 
 |-  ( [_ A / x ]_ ( C i^i D ) = { y | [. A / x ]. ( y e. C /\ y e. D ) } -> ( { y | [. A / x ]. ( y e. C /\ y e. D ) } = { y | ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) } -> [_ A / x ]_ ( C i^i D ) = { y | ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) } ) )
36 14 33 35 e11 
 |-  (. A e. B ->. [_ A / x ]_ ( C i^i D ) = { y | ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) } ).
37 df-in 
 |-  ( [_ A / x ]_ C i^i [_ A / x ]_ D ) = { y | ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) }
38 eqeq2 
 |-  ( ( [_ A / x ]_ C i^i [_ A / x ]_ D ) = { y | ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) } -> ( [_ A / x ]_ ( C i^i D ) = ( [_ A / x ]_ C i^i [_ A / x ]_ D ) <-> [_ A / x ]_ ( C i^i D ) = { y | ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) } ) )
39 38 biimprcd 
 |-  ( [_ A / x ]_ ( C i^i D ) = { y | ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) } -> ( ( [_ A / x ]_ C i^i [_ A / x ]_ D ) = { y | ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) } -> [_ A / x ]_ ( C i^i D ) = ( [_ A / x ]_ C i^i [_ A / x ]_ D ) ) )
40 36 37 39 e10 
 |-  (. A e. B ->. [_ A / x ]_ ( C i^i D ) = ( [_ A / x ]_ C i^i [_ A / x ]_ D ) ).
41 40 in1 
 |-  ( A e. B -> [_ A / x ]_ ( C i^i D ) = ( [_ A / x ]_ C i^i [_ A / x ]_ D ) )