| Step |
Hyp |
Ref |
Expression |
| 1 |
|
vex |
|- w e. _V |
| 2 |
1
|
elpr |
|- ( w e. { x , y } <-> ( w = x \/ w = y ) ) |
| 3 |
2
|
biimpri |
|- ( ( w = x \/ w = y ) -> w e. { x , y } ) |
| 4 |
3
|
rgenw |
|- A. w e. M ( ( w = x \/ w = y ) -> w e. { x , y } ) |
| 5 |
|
eleq2 |
|- ( z = { x , y } -> ( w e. z <-> w e. { x , y } ) ) |
| 6 |
5
|
imbi2d |
|- ( z = { x , y } -> ( ( ( w = x \/ w = y ) -> w e. z ) <-> ( ( w = x \/ w = y ) -> w e. { x , y } ) ) ) |
| 7 |
6
|
ralbidv |
|- ( z = { x , y } -> ( A. w e. M ( ( w = x \/ w = y ) -> w e. z ) <-> A. w e. M ( ( w = x \/ w = y ) -> w e. { x , y } ) ) ) |
| 8 |
7
|
rspcev |
|- ( ( { x , y } e. M /\ A. w e. M ( ( w = x \/ w = y ) -> w e. { x , y } ) ) -> E. z e. M A. w e. M ( ( w = x \/ w = y ) -> w e. z ) ) |
| 9 |
4 8
|
mpan2 |
|- ( { x , y } e. M -> E. z e. M A. w e. M ( ( w = x \/ w = y ) -> w e. z ) ) |
| 10 |
9
|
2ralimi |
|- ( A. x e. M A. y e. M { x , y } e. M -> A. x e. M A. y e. M E. z e. M A. w e. M ( ( w = x \/ w = y ) -> w e. z ) ) |