Step |
Hyp |
Ref |
Expression |
1 |
|
riin0 |
|- ( X = (/) -> ( A i^i |^|_ x e. X { y e. A | ph } ) = A ) |
2 |
|
rzal |
|- ( X = (/) -> A. x e. X ph ) |
3 |
2
|
ralrimivw |
|- ( X = (/) -> A. y e. A A. x e. X ph ) |
4 |
|
rabid2 |
|- ( A = { y e. A | A. x e. X ph } <-> A. y e. A A. x e. X ph ) |
5 |
3 4
|
sylibr |
|- ( X = (/) -> A = { y e. A | A. x e. X ph } ) |
6 |
1 5
|
eqtrd |
|- ( X = (/) -> ( A i^i |^|_ x e. X { y e. A | ph } ) = { y e. A | A. x e. X ph } ) |
7 |
|
ssrab2 |
|- { y e. A | ph } C_ A |
8 |
7
|
rgenw |
|- A. x e. X { y e. A | ph } C_ A |
9 |
|
riinn0 |
|- ( ( A. x e. X { y e. A | ph } C_ A /\ X =/= (/) ) -> ( A i^i |^|_ x e. X { y e. A | ph } ) = |^|_ x e. X { y e. A | ph } ) |
10 |
8 9
|
mpan |
|- ( X =/= (/) -> ( A i^i |^|_ x e. X { y e. A | ph } ) = |^|_ x e. X { y e. A | ph } ) |
11 |
|
iinrab |
|- ( X =/= (/) -> |^|_ x e. X { y e. A | ph } = { y e. A | A. x e. X ph } ) |
12 |
10 11
|
eqtrd |
|- ( X =/= (/) -> ( A i^i |^|_ x e. X { y e. A | ph } ) = { y e. A | A. x e. X ph } ) |
13 |
6 12
|
pm2.61ine |
|- ( A i^i |^|_ x e. X { y e. A | ph } ) = { y e. A | A. x e. X ph } |