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 9082

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

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

**Proof of Theorem 0sdomg**
Step	Hyp	Ref	Expression
1		0domg 9080	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∅ ≼ 𝐴)
2		brsdom 8959	. . . 4 ⊢ (∅ ≺ 𝐴 ↔ (∅ ≼ 𝐴 ∧ ¬ ∅ ≈ 𝐴))
3	2	baib 544	. . 3 ⊢ (∅ ≼ 𝐴 → (∅ ≺ 𝐴 ↔ ¬ ∅ ≈ 𝐴))
4	1, 3	syl 18	. 2 ⊢ (𝐴 ∈ 𝑉 → (∅ ≺ 𝐴 ↔ ¬ ∅ ≈ 𝐴))
5		en0r 9005	. . 3 ⊢ (∅ ≈ 𝐴 ↔ 𝐴 = ∅)
6	5	necon3bbii 3007	. 2 ⊢ (¬ ∅ ≈ 𝐴 ↔ 𝐴 ≠ ∅)
7	4, 6	bitrdi 290	1 ⊢ (𝐴 ∈ 𝑉 → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∈ wcel 2145 ≠ wne 2960 ∅c0 4288 class class class wbr 5105 ≈ cen 8928 ≼ cdom 8929 ≺ csdm 8930

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-ext 2737 ax-sep 5251 ax-nul 5261 ax-pr 5395

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-sb 2094 df-mo 2569 df-clab 2744 df-cleq 2757 df-clel 2840 df-ne 2961 df-ral 3080 df-rex 3090 df-rab 3418 df-v 3459 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-sn 4586 df-pr 4588 df-op 4592 df-br 5106 df-opab 5168 df-id 5547 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-en 8932 df-dom 8933 df-sdom 8934

This theorem is referenced by: 0sdom 9084 fodomr 9104 pwdom 9105 0sdom1dom 9194 1sdom2dom 9202 infn0ALT 9251 fodomfir 9275 fodomfib 9276 domwdom 9524 iunfictbso 10086 djulepw 10164 fin45 10364 fodomb 10498 brdom3 10500 gchxpidm 10642 inar1 10748 csdfil 24012 ovoliunnul 25627 carsgclctunlem3 34627 domalom 37910 ovoliunnfl 38173 voliunnfl 38175 volsupnfl 38176 sdomne0 44001 sdomne0d 44002 ensucne0OLD 44118 nnfoctb 45626 caragenunicl 47096

W3C validator