0sdomg - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > 0sdomg		Structured version Visualization version GIF version

Theorem 0sdomg 9026

Description: A set strictly dominates the empty set iff it is not empty. (Contributed by NM, 23-Mar-2006.) Avoid ax-pow 5305, ax-un 7674. (Revised by BTernaryTau, 29-Nov-2024.)

**Assertion**
Ref	Expression
0sdomg	⊢ (𝐴 ∈ 𝑉 → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))

**Proof of Theorem 0sdomg**
Step	Hyp	Ref	Expression
1		0domg 9024	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∅ ≼ 𝐴)
2		brsdom 8903	. . . 4 ⊢ (∅ ≺ 𝐴 ↔ (∅ ≼ 𝐴 ∧ ¬ ∅ ≈ 𝐴))
3	2	baib 535	. . 3 ⊢ (∅ ≼ 𝐴 → (∅ ≺ 𝐴 ↔ ¬ ∅ ≈ 𝐴))
4	1, 3	syl 17	. 2 ⊢ (𝐴 ∈ 𝑉 → (∅ ≺ 𝐴 ↔ ¬ ∅ ≈ 𝐴))
5		en0r 8949	. . 3 ⊢ (∅ ≈ 𝐴 ↔ 𝐴 = ∅)
6	5	necon3bbii 2976	. 2 ⊢ (¬ ∅ ≈ 𝐴 ↔ 𝐴 ≠ ∅)
7	4, 6	bitrdi 287	1 ⊢ (𝐴 ∈ 𝑉 → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∈ wcel 2113 ≠ wne 2929 ∅c0 4282 class class class wbr 5093 ≈ cen 8872 ≼ cdom 8873 ≺ csdm 8874

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-ext 2705 ax-sep 5236 ax-nul 5246 ax-pr 5372

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-sb 2068 df-mo 2537 df-clab 2712 df-cleq 2725 df-clel 2808 df-ne 2930 df-ral 3049 df-rex 3058 df-rab 3397 df-v 3439 df-dif 3901 df-un 3903 df-ss 3915 df-nul 4283 df-if 4475 df-sn 4576 df-pr 4578 df-op 4582 df-br 5094 df-opab 5156 df-id 5514 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-en 8876 df-dom 8877 df-sdom 8878

This theorem is referenced by: 0sdom 9028 fodomr 9048 pwdom 9049 0sdom1dom 9137 1sdom2dom 9145 infn0ALT 9194 fodomfir 9219 fodomfib 9220 fodomfibOLD 9222 domwdom 9467 iunfictbso 10012 djulepw 10091 fin45 10290 fodomb 10424 brdom3 10426 gchxpidm 10567 inar1 10673 csdfil 23810 ovoliunnul 25436 carsgclctunlem3 34354 domalom 37469 ovoliunnfl 37722 voliunnfl 37724 volsupnfl 37725 sdomne0 43530 sdomne0d 43531 ensucne0OLD 43647 nnfoctb 45169 caragenunicl 46646

W3C validator