Step |
Hyp |
Ref |
Expression |
1 |
|
brfvopab.1 |
|- ( X e. _V -> ( F ` X ) = { <. y , z >. | ph } ) |
2 |
1
|
breqd |
|- ( X e. _V -> ( A ( F ` X ) B <-> A { <. y , z >. | ph } B ) ) |
3 |
|
brabv |
|- ( A { <. y , z >. | ph } B -> ( A e. _V /\ B e. _V ) ) |
4 |
2 3
|
syl6bi |
|- ( X e. _V -> ( A ( F ` X ) B -> ( A e. _V /\ B e. _V ) ) ) |
5 |
4
|
imdistani |
|- ( ( X e. _V /\ A ( F ` X ) B ) -> ( X e. _V /\ ( A e. _V /\ B e. _V ) ) ) |
6 |
|
3anass |
|- ( ( X e. _V /\ A e. _V /\ B e. _V ) <-> ( X e. _V /\ ( A e. _V /\ B e. _V ) ) ) |
7 |
5 6
|
sylibr |
|- ( ( X e. _V /\ A ( F ` X ) B ) -> ( X e. _V /\ A e. _V /\ B e. _V ) ) |
8 |
7
|
ex |
|- ( X e. _V -> ( A ( F ` X ) B -> ( X e. _V /\ A e. _V /\ B e. _V ) ) ) |
9 |
|
fvprc |
|- ( -. X e. _V -> ( F ` X ) = (/) ) |
10 |
|
breq |
|- ( ( F ` X ) = (/) -> ( A ( F ` X ) B <-> A (/) B ) ) |
11 |
|
br0 |
|- -. A (/) B |
12 |
11
|
pm2.21i |
|- ( A (/) B -> ( X e. _V /\ A e. _V /\ B e. _V ) ) |
13 |
10 12
|
syl6bi |
|- ( ( F ` X ) = (/) -> ( A ( F ` X ) B -> ( X e. _V /\ A e. _V /\ B e. _V ) ) ) |
14 |
9 13
|
syl |
|- ( -. X e. _V -> ( A ( F ` X ) B -> ( X e. _V /\ A e. _V /\ B e. _V ) ) ) |
15 |
8 14
|
pm2.61i |
|- ( A ( F ` X ) B -> ( X e. _V /\ A e. _V /\ B e. _V ) ) |