Step |
Hyp |
Ref |
Expression |
1 |
|
csbie2df.p |
|- F/ x ph |
2 |
|
csbie2df.c |
|- ( ph -> F/_ x C ) |
3 |
|
csbie2df.d |
|- ( ph -> F/_ x D ) |
4 |
|
csbie2df.a |
|- ( ph -> A e. V ) |
5 |
|
csbie2df.1 |
|- ( ( ph /\ x = y ) -> B = C ) |
6 |
|
csbie2df.2 |
|- ( ( ph /\ y = A ) -> C = D ) |
7 |
|
eqidd |
|- ( ph -> D = D ) |
8 |
|
dfsbcq |
|- ( y = A -> ( [. y / x ]. B = D <-> [. A / x ]. B = D ) ) |
9 |
|
sbceqg |
|- ( A e. V -> ( [. A / x ]. B = D <-> [_ A / x ]_ B = [_ A / x ]_ D ) ) |
10 |
9
|
adantr |
|- ( ( A e. V /\ ph ) -> ( [. A / x ]. B = D <-> [_ A / x ]_ B = [_ A / x ]_ D ) ) |
11 |
|
csbtt |
|- ( ( A e. V /\ F/_ x D ) -> [_ A / x ]_ D = D ) |
12 |
3 11
|
sylan2 |
|- ( ( A e. V /\ ph ) -> [_ A / x ]_ D = D ) |
13 |
12
|
eqeq2d |
|- ( ( A e. V /\ ph ) -> ( [_ A / x ]_ B = [_ A / x ]_ D <-> [_ A / x ]_ B = D ) ) |
14 |
10 13
|
bitrd |
|- ( ( A e. V /\ ph ) -> ( [. A / x ]. B = D <-> [_ A / x ]_ B = D ) ) |
15 |
4 14
|
mpancom |
|- ( ph -> ( [. A / x ]. B = D <-> [_ A / x ]_ B = D ) ) |
16 |
8 15
|
sylan9bb |
|- ( ( y = A /\ ph ) -> ( [. y / x ]. B = D <-> [_ A / x ]_ B = D ) ) |
17 |
16
|
pm5.74da |
|- ( y = A -> ( ( ph -> [. y / x ]. B = D ) <-> ( ph -> [_ A / x ]_ B = D ) ) ) |
18 |
6
|
eqeq1d |
|- ( ( ph /\ y = A ) -> ( C = D <-> D = D ) ) |
19 |
18
|
expcom |
|- ( y = A -> ( ph -> ( C = D <-> D = D ) ) ) |
20 |
19
|
pm5.74d |
|- ( y = A -> ( ( ph -> C = D ) <-> ( ph -> D = D ) ) ) |
21 |
|
sbsbc |
|- ( [ y / x ] B = D <-> [. y / x ]. B = D ) |
22 |
2 3
|
nfeqd |
|- ( ph -> F/ x C = D ) |
23 |
5
|
eqeq1d |
|- ( ( ph /\ x = y ) -> ( B = D <-> C = D ) ) |
24 |
23
|
ex |
|- ( ph -> ( x = y -> ( B = D <-> C = D ) ) ) |
25 |
1 22 24
|
sbiedw |
|- ( ph -> ( [ y / x ] B = D <-> C = D ) ) |
26 |
21 25
|
bitr3id |
|- ( ph -> ( [. y / x ]. B = D <-> C = D ) ) |
27 |
26
|
pm5.74i |
|- ( ( ph -> [. y / x ]. B = D ) <-> ( ph -> C = D ) ) |
28 |
17 20 27
|
vtoclbg |
|- ( A e. V -> ( ( ph -> [_ A / x ]_ B = D ) <-> ( ph -> D = D ) ) ) |
29 |
7 28
|
mpbiri |
|- ( A e. V -> ( ph -> [_ A / x ]_ B = D ) ) |
30 |
4 29
|
mpcom |
|- ( ph -> [_ A / x ]_ B = D ) |