Step |
Hyp |
Ref |
Expression |
1 |
|
sbcal |
|- ( [. A / x ]. A. y ( y e. B -> y e. C ) <-> A. y [. A / x ]. ( y e. B -> y e. C ) ) |
2 |
|
sbcimg |
|- ( A e. V -> ( [. A / x ]. ( y e. B -> y e. C ) <-> ( [. A / x ]. y e. B -> [. A / x ]. y e. C ) ) ) |
3 |
|
sbcel2 |
|- ( [. A / x ]. y e. B <-> y e. [_ A / x ]_ B ) |
4 |
|
sbcel2 |
|- ( [. A / x ]. y e. C <-> y e. [_ A / x ]_ C ) |
5 |
3 4
|
imbi12i |
|- ( ( [. A / x ]. y e. B -> [. A / x ]. y e. C ) <-> ( y e. [_ A / x ]_ B -> y e. [_ A / x ]_ C ) ) |
6 |
2 5
|
bitrdi |
|- ( A e. V -> ( [. A / x ]. ( y e. B -> y e. C ) <-> ( y e. [_ A / x ]_ B -> y e. [_ A / x ]_ C ) ) ) |
7 |
6
|
albidv |
|- ( A e. V -> ( A. y [. A / x ]. ( y e. B -> y e. C ) <-> A. y ( y e. [_ A / x ]_ B -> y e. [_ A / x ]_ C ) ) ) |
8 |
1 7
|
syl5bb |
|- ( A e. V -> ( [. A / x ]. A. y ( y e. B -> y e. C ) <-> A. y ( y e. [_ A / x ]_ B -> y e. [_ A / x ]_ C ) ) ) |
9 |
|
dfss2 |
|- ( B C_ C <-> A. y ( y e. B -> y e. C ) ) |
10 |
9
|
sbcbii |
|- ( [. A / x ]. B C_ C <-> [. A / x ]. A. y ( y e. B -> y e. C ) ) |
11 |
|
dfss2 |
|- ( [_ A / x ]_ B C_ [_ A / x ]_ C <-> A. y ( y e. [_ A / x ]_ B -> y e. [_ A / x ]_ C ) ) |
12 |
8 10 11
|
3bitr4g |
|- ( A e. V -> ( [. A / x ]. B C_ C <-> [_ A / x ]_ B C_ [_ A / x ]_ C ) ) |