Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > 0neqopab | Structured version Visualization version Unicode version | ||
| Description: The empty set is never an element in an ordered-pair class abstraction. (Contributed by Alexander van der Vekens, 5-Nov-2017.) |
| Ref | Expression |
|---|---|
| 0neqopab |
             |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elopab 4708 |
. . 3
  "){kind=small} | |
| 2 | nfopab1 4468 |
. . . . . 6
| |
| 3 | 2 | nfel2 2607 |
. . . . 5
 |
| 4 | 3 | nfn 1982 |
. . . 4
|
| 5 | nfopab2 4469 |
. . . . . . 7
| |
| 6 | 5 | nfel2 2607 |
. . . . . 6
|
| 7 | 6 | nfn 1982 |
. . . . 5
|
| 8 | vex 3047 |
. . . . . . . 8
 | |
| 9 | vex 3047 |
. . . . . . . 8
| |
| 10 | 8, 9 | opnzi 4673 |
. . . . . . 7
 |
| 11 | nesym 2679 |
. . . . . . . 8
| |
| 12 | pm2.21 112 |
. . . . . . . 8
 | |
| 13 | 11, 12 | sylbi 199 |
. . . . . . 7
|
| 14 | 10, 13 | ax-mp 5 |
. . . . . 6
|
| 15 | 14 | adantr 467 |
. . . . 5
|
| 16 | 7, 15 | exlimi 1994 |
. . . 4
|
| 17 | 4, 16 | exlimi 1994 |
. . 3
|
| 18 | 1, 17 | sylbi 199 |
. 2
|
| 19 | id 22 |
. 2
| |
| 20 | 18, 19 | pm2.61i 168 |
1
|
| Colors of variables: wff setvar class |
| Syntax hints: wn 3
wi 4
wa 371
wceq 1443
wex 1662
wcel 1886
wne 2621
c0 3730
cop 3973
copab 4459 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-sep 4524 ax-nul 4533 ax-pr 4638 |
| This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-v 3046 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-nul 3731 df-if 3881 df-sn 3968 df-pr 3970 df-op 3974 df-opab 4461 |
| This theorem is referenced by: brabv 6333 bj-0nelmpt 31621 |
| Copyright terms: Public domain | W3C validator |