Step |
Hyp |
Ref |
Expression |
1 |
|
elabrex.1 |
|- B e. _V |
2 |
|
tru |
|- T. |
3 |
|
csbeq1a |
|- ( x = z -> B = [_ z / x ]_ B ) |
4 |
3
|
equcoms |
|- ( z = x -> B = [_ z / x ]_ B ) |
5 |
|
trud |
|- ( z = x -> T. ) |
6 |
4 5
|
2thd |
|- ( z = x -> ( B = [_ z / x ]_ B <-> T. ) ) |
7 |
6
|
rspcev |
|- ( ( x e. A /\ T. ) -> E. z e. A B = [_ z / x ]_ B ) |
8 |
2 7
|
mpan2 |
|- ( x e. A -> E. z e. A B = [_ z / x ]_ B ) |
9 |
|
eqeq1 |
|- ( y = B -> ( y = [_ z / x ]_ B <-> B = [_ z / x ]_ B ) ) |
10 |
9
|
rexbidv |
|- ( y = B -> ( E. z e. A y = [_ z / x ]_ B <-> E. z e. A B = [_ z / x ]_ B ) ) |
11 |
1 10
|
elab |
|- ( B e. { y | E. z e. A y = [_ z / x ]_ B } <-> E. z e. A B = [_ z / x ]_ B ) |
12 |
8 11
|
sylibr |
|- ( x e. A -> B e. { y | E. z e. A y = [_ z / x ]_ B } ) |
13 |
|
nfv |
|- F/ z y = B |
14 |
|
nfcsb1v |
|- F/_ x [_ z / x ]_ B |
15 |
14
|
nfeq2 |
|- F/ x y = [_ z / x ]_ B |
16 |
3
|
eqeq2d |
|- ( x = z -> ( y = B <-> y = [_ z / x ]_ B ) ) |
17 |
13 15 16
|
cbvrexw |
|- ( E. x e. A y = B <-> E. z e. A y = [_ z / x ]_ B ) |
18 |
17
|
abbii |
|- { y | E. x e. A y = B } = { y | E. z e. A y = [_ z / x ]_ B } |
19 |
12 18
|
eleqtrrdi |
|- ( x e. A -> B e. { y | E. x e. A y = B } ) |