Step |
Hyp |
Ref |
Expression |
1 |
|
tru |
|- T. |
2 |
|
csbeq1a |
|- ( x = z -> B = [_ z / x ]_ B ) |
3 |
2
|
equcoms |
|- ( z = x -> B = [_ z / x ]_ B ) |
4 |
|
trud |
|- ( z = x -> T. ) |
5 |
3 4
|
2thd |
|- ( z = x -> ( B = [_ z / x ]_ B <-> T. ) ) |
6 |
5
|
rspcev |
|- ( ( x e. A /\ T. ) -> E. z e. A B = [_ z / x ]_ B ) |
7 |
1 6
|
mpan2 |
|- ( x e. A -> E. z e. A B = [_ z / x ]_ B ) |
8 |
7
|
adantr |
|- ( ( x e. A /\ B e. V ) -> 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 |
10
|
elabg |
|- ( B e. V -> ( B e. { y | E. z e. A y = [_ z / x ]_ B } <-> E. z e. A B = [_ z / x ]_ B ) ) |
12 |
11
|
adantl |
|- ( ( x e. A /\ B e. V ) -> ( B e. { y | E. z e. A y = [_ z / x ]_ B } <-> E. z e. A B = [_ z / x ]_ B ) ) |
13 |
8 12
|
mpbird |
|- ( ( x e. A /\ B e. V ) -> B e. { y | E. z e. A y = [_ z / x ]_ B } ) |
14 |
|
nfv |
|- F/ z y = B |
15 |
|
nfcsb1v |
|- F/_ x [_ z / x ]_ B |
16 |
15
|
nfeq2 |
|- F/ x y = [_ z / x ]_ B |
17 |
2
|
eqeq2d |
|- ( x = z -> ( y = B <-> y = [_ z / x ]_ B ) ) |
18 |
14 16 17
|
cbvrexw |
|- ( E. x e. A y = B <-> E. z e. A y = [_ z / x ]_ B ) |
19 |
18
|
abbii |
|- { y | E. x e. A y = B } = { y | E. z e. A y = [_ z / x ]_ B } |
20 |
13 19
|
eleqtrrdi |
|- ( ( x e. A /\ B e. V ) -> B e. { y | E. x e. A y = B } ) |