Step |
Hyp |
Ref |
Expression |
1 |
|
sbccom2f.1 |
|- A e. _V |
2 |
|
sbccom2f.2 |
|- F/_ y A |
3 |
|
sbcco |
|- ( [. B / z ]. [. z / y ]. ph <-> [. B / y ]. ph ) |
4 |
3
|
bicomi |
|- ( [. B / y ]. ph <-> [. B / z ]. [. z / y ]. ph ) |
5 |
4
|
sbcbii |
|- ( [. A / x ]. [. B / y ]. ph <-> [. A / x ]. [. B / z ]. [. z / y ]. ph ) |
6 |
1
|
sbccom2 |
|- ( [. A / x ]. [. B / z ]. [. z / y ]. ph <-> [. [_ A / x ]_ B / z ]. [. A / x ]. [. z / y ]. ph ) |
7 |
|
vex |
|- z e. _V |
8 |
7
|
sbccom2 |
|- ( [. z / y ]. [. A / x ]. ph <-> [. [_ z / y ]_ A / x ]. [. z / y ]. ph ) |
9 |
7 2
|
csbgfi |
|- [_ z / y ]_ A = A |
10 |
|
dfsbcq |
|- ( [_ z / y ]_ A = A -> ( [. [_ z / y ]_ A / x ]. [. z / y ]. ph <-> [. A / x ]. [. z / y ]. ph ) ) |
11 |
9 10
|
ax-mp |
|- ( [. [_ z / y ]_ A / x ]. [. z / y ]. ph <-> [. A / x ]. [. z / y ]. ph ) |
12 |
8 11
|
bitri |
|- ( [. z / y ]. [. A / x ]. ph <-> [. A / x ]. [. z / y ]. ph ) |
13 |
12
|
bicomi |
|- ( [. A / x ]. [. z / y ]. ph <-> [. z / y ]. [. A / x ]. ph ) |
14 |
13
|
sbcbii |
|- ( [. [_ A / x ]_ B / z ]. [. A / x ]. [. z / y ]. ph <-> [. [_ A / x ]_ B / z ]. [. z / y ]. [. A / x ]. ph ) |
15 |
|
sbcco |
|- ( [. [_ A / x ]_ B / z ]. [. z / y ]. [. A / x ]. ph <-> [. [_ A / x ]_ B / y ]. [. A / x ]. ph ) |
16 |
14 15
|
bitri |
|- ( [. [_ A / x ]_ B / z ]. [. A / x ]. [. z / y ]. ph <-> [. [_ A / x ]_ B / y ]. [. A / x ]. ph ) |
17 |
5 6 16
|
3bitri |
|- ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. [. A / x ]. ph ) |