Step |
Hyp |
Ref |
Expression |
1 |
|
wununi.1 |
|- ( ph -> U e. WUni ) |
2 |
|
wununi.2 |
|- ( ph -> A e. U ) |
3 |
|
wunpr.3 |
|- ( ph -> B e. U ) |
4 |
|
iswun |
|- ( U e. WUni -> ( U e. WUni <-> ( Tr U /\ U =/= (/) /\ A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) ) ) ) |
5 |
4
|
ibi |
|- ( U e. WUni -> ( Tr U /\ U =/= (/) /\ A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) ) ) |
6 |
5
|
simp3d |
|- ( U e. WUni -> A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) ) |
7 |
|
simp3 |
|- ( ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) -> A. y e. U { x , y } e. U ) |
8 |
7
|
ralimi |
|- ( A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) -> A. x e. U A. y e. U { x , y } e. U ) |
9 |
1 6 8
|
3syl |
|- ( ph -> A. x e. U A. y e. U { x , y } e. U ) |
10 |
|
preq1 |
|- ( x = A -> { x , y } = { A , y } ) |
11 |
10
|
eleq1d |
|- ( x = A -> ( { x , y } e. U <-> { A , y } e. U ) ) |
12 |
|
preq2 |
|- ( y = B -> { A , y } = { A , B } ) |
13 |
12
|
eleq1d |
|- ( y = B -> ( { A , y } e. U <-> { A , B } e. U ) ) |
14 |
11 13
|
rspc2va |
|- ( ( ( A e. U /\ B e. U ) /\ A. x e. U A. y e. U { x , y } e. U ) -> { A , B } e. U ) |
15 |
2 3 9 14
|
syl21anc |
|- ( ph -> { A , B } e. U ) |