Step |
Hyp |
Ref |
Expression |
1 |
|
rabsnif.f |
|- ( x = A -> ( ph <-> ps ) ) |
2 |
|
rabsnifsb |
|- { x e. { A } | ph } = if ( [. A / x ]. ph , { A } , (/) ) |
3 |
1
|
sbcieg |
|- ( A e. _V -> ( [. A / x ]. ph <-> ps ) ) |
4 |
3
|
ifbid |
|- ( A e. _V -> if ( [. A / x ]. ph , { A } , (/) ) = if ( ps , { A } , (/) ) ) |
5 |
2 4
|
eqtrid |
|- ( A e. _V -> { x e. { A } | ph } = if ( ps , { A } , (/) ) ) |
6 |
|
rab0 |
|- { x e. (/) | ph } = (/) |
7 |
|
ifid |
|- if ( ps , (/) , (/) ) = (/) |
8 |
6 7
|
eqtr4i |
|- { x e. (/) | ph } = if ( ps , (/) , (/) ) |
9 |
|
snprc |
|- ( -. A e. _V <-> { A } = (/) ) |
10 |
9
|
biimpi |
|- ( -. A e. _V -> { A } = (/) ) |
11 |
10
|
rabeqdv |
|- ( -. A e. _V -> { x e. { A } | ph } = { x e. (/) | ph } ) |
12 |
10
|
ifeq1d |
|- ( -. A e. _V -> if ( ps , { A } , (/) ) = if ( ps , (/) , (/) ) ) |
13 |
8 11 12
|
3eqtr4a |
|- ( -. A e. _V -> { x e. { A } | ph } = if ( ps , { A } , (/) ) ) |
14 |
5 13
|
pm2.61i |
|- { x e. { A } | ph } = if ( ps , { A } , (/) ) |