Step |
Hyp |
Ref |
Expression |
1 |
|
csbab |
|- [_ A / x ]_ { c | E. y E. z E. d ( c = <. <. y , z >. , d >. /\ ph ) } = { c | [. A / x ]. E. y E. z E. d ( c = <. <. y , z >. , d >. /\ ph ) } |
2 |
|
sbcex2 |
|- ( [. A / x ]. E. y E. z E. d ( c = <. <. y , z >. , d >. /\ ph ) <-> E. y [. A / x ]. E. z E. d ( c = <. <. y , z >. , d >. /\ ph ) ) |
3 |
|
sbcex2 |
|- ( [. A / x ]. E. z E. d ( c = <. <. y , z >. , d >. /\ ph ) <-> E. z [. A / x ]. E. d ( c = <. <. y , z >. , d >. /\ ph ) ) |
4 |
|
sbcex2 |
|- ( [. A / x ]. E. d ( c = <. <. y , z >. , d >. /\ ph ) <-> E. d [. A / x ]. ( c = <. <. y , z >. , d >. /\ ph ) ) |
5 |
|
sbcan |
|- ( [. A / x ]. ( c = <. <. y , z >. , d >. /\ ph ) <-> ( [. A / x ]. c = <. <. y , z >. , d >. /\ [. A / x ]. ph ) ) |
6 |
|
sbcg |
|- ( A e. V -> ( [. A / x ]. c = <. <. y , z >. , d >. <-> c = <. <. y , z >. , d >. ) ) |
7 |
6
|
anbi1d |
|- ( A e. V -> ( ( [. A / x ]. c = <. <. y , z >. , d >. /\ [. A / x ]. ph ) <-> ( c = <. <. y , z >. , d >. /\ [. A / x ]. ph ) ) ) |
8 |
5 7
|
syl5bb |
|- ( A e. V -> ( [. A / x ]. ( c = <. <. y , z >. , d >. /\ ph ) <-> ( c = <. <. y , z >. , d >. /\ [. A / x ]. ph ) ) ) |
9 |
8
|
exbidv |
|- ( A e. V -> ( E. d [. A / x ]. ( c = <. <. y , z >. , d >. /\ ph ) <-> E. d ( c = <. <. y , z >. , d >. /\ [. A / x ]. ph ) ) ) |
10 |
4 9
|
syl5bb |
|- ( A e. V -> ( [. A / x ]. E. d ( c = <. <. y , z >. , d >. /\ ph ) <-> E. d ( c = <. <. y , z >. , d >. /\ [. A / x ]. ph ) ) ) |
11 |
10
|
exbidv |
|- ( A e. V -> ( E. z [. A / x ]. E. d ( c = <. <. y , z >. , d >. /\ ph ) <-> E. z E. d ( c = <. <. y , z >. , d >. /\ [. A / x ]. ph ) ) ) |
12 |
3 11
|
syl5bb |
|- ( A e. V -> ( [. A / x ]. E. z E. d ( c = <. <. y , z >. , d >. /\ ph ) <-> E. z E. d ( c = <. <. y , z >. , d >. /\ [. A / x ]. ph ) ) ) |
13 |
12
|
exbidv |
|- ( A e. V -> ( E. y [. A / x ]. E. z E. d ( c = <. <. y , z >. , d >. /\ ph ) <-> E. y E. z E. d ( c = <. <. y , z >. , d >. /\ [. A / x ]. ph ) ) ) |
14 |
2 13
|
syl5bb |
|- ( A e. V -> ( [. A / x ]. E. y E. z E. d ( c = <. <. y , z >. , d >. /\ ph ) <-> E. y E. z E. d ( c = <. <. y , z >. , d >. /\ [. A / x ]. ph ) ) ) |
15 |
14
|
abbidv |
|- ( A e. V -> { c | [. A / x ]. E. y E. z E. d ( c = <. <. y , z >. , d >. /\ ph ) } = { c | E. y E. z E. d ( c = <. <. y , z >. , d >. /\ [. A / x ]. ph ) } ) |
16 |
1 15
|
syl5eq |
|- ( A e. V -> [_ A / x ]_ { c | E. y E. z E. d ( c = <. <. y , z >. , d >. /\ ph ) } = { c | E. y E. z E. d ( c = <. <. y , z >. , d >. /\ [. A / x ]. ph ) } ) |
17 |
|
df-oprab |
|- { <. <. y , z >. , d >. | ph } = { c | E. y E. z E. d ( c = <. <. y , z >. , d >. /\ ph ) } |
18 |
17
|
csbeq2i |
|- [_ A / x ]_ { <. <. y , z >. , d >. | ph } = [_ A / x ]_ { c | E. y E. z E. d ( c = <. <. y , z >. , d >. /\ ph ) } |
19 |
|
df-oprab |
|- { <. <. y , z >. , d >. | [. A / x ]. ph } = { c | E. y E. z E. d ( c = <. <. y , z >. , d >. /\ [. A / x ]. ph ) } |
20 |
16 18 19
|
3eqtr4g |
|- ( A e. V -> [_ A / x ]_ { <. <. y , z >. , d >. | ph } = { <. <. y , z >. , d >. | [. A / x ]. ph } ) |