Description: Proof of pwuninel under the assumption that the union of the given class is a set, avoiding ax-pr and ax-un . (Contributed by Stefan O'Rear, 22-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | pwuninel2 | |- ( U. A e. V -> -. ~P U. A e. A ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pwnss | |- ( U. A e. V -> -. ~P U. A C_ U. A ) |
|
2 | elssuni | |- ( ~P U. A e. A -> ~P U. A C_ U. A ) |
|
3 | 1 2 | nsyl | |- ( U. A e. V -> -. ~P U. A e. A ) |