![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > prnzg | Structured version Visualization version GIF version |
Description: A pair containing a set is not empty. (Contributed by FL, 19-Sep-2011.) (Proof shortened by JJ, 23-Jul-2021.) |
Ref | Expression |
---|---|
prnzg | ⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐵} ≠ ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prid1g 4656 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵}) | |
2 | 1 | ne0d 4251 | 1 ⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐵} ≠ ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2111 ≠ wne 2987 ∅c0 4243 {cpr 4527 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-tru 1541 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-ne 2988 df-v 3443 df-dif 3884 df-un 3886 df-nul 4244 df-sn 4526 df-pr 4528 |
This theorem is referenced by: preqsnd 4749 0nelop 5351 fr2nr 5497 mreincl 16862 subrgin 19551 lssincl 19730 incld 21648 umgrnloopv 26899 upgr1elem 26905 usgrnloopvALT 26991 difelsiga 31502 inelpisys 31523 inidl 35468 coss0 35879 pmapmeet 37069 diameetN 38352 dihmeetlem2N 38595 dihmeetcN 38598 dihmeet 38639 |
Copyright terms: Public domain | W3C validator |