Step |
Hyp |
Ref |
Expression |
1 |
|
rabn0 |
|- ( { x e. On | ph } =/= (/) <-> E. x e. On ph ) |
2 |
|
ssrab2 |
|- { x e. On | ph } C_ On |
3 |
|
onint |
|- ( ( { x e. On | ph } C_ On /\ { x e. On | ph } =/= (/) ) -> |^| { x e. On | ph } e. { x e. On | ph } ) |
4 |
2 3
|
mpan |
|- ( { x e. On | ph } =/= (/) -> |^| { x e. On | ph } e. { x e. On | ph } ) |
5 |
1 4
|
sylbir |
|- ( E. x e. On ph -> |^| { x e. On | ph } e. { x e. On | ph } ) |
6 |
|
nfcv |
|- F/_ x On |
7 |
6
|
elrabsf |
|- ( |^| { x e. On | ph } e. { x e. On | ph } <-> ( |^| { x e. On | ph } e. On /\ [. |^| { x e. On | ph } / x ]. ph ) ) |
8 |
7
|
simprbi |
|- ( |^| { x e. On | ph } e. { x e. On | ph } -> [. |^| { x e. On | ph } / x ]. ph ) |
9 |
5 8
|
syl |
|- ( E. x e. On ph -> [. |^| { x e. On | ph } / x ]. ph ) |