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 9044

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

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

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

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∈ wcel 2114 ≠ wne 2932 ∅c0 4273 class class class wbr 5085 ≈ cen 8890 ≼ cdom 8891 ≺ csdm 8892

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-ext 2708 ax-sep 5231 ax-nul 5241 ax-pr 5375

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-sb 2069 df-mo 2539 df-clab 2715 df-cleq 2728 df-clel 2811 df-ne 2933 df-ral 3052 df-rex 3062 df-rab 3390 df-v 3431 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-nul 4274 df-if 4467 df-sn 4568 df-pr 4570 df-op 4574 df-br 5086 df-opab 5148 df-id 5526 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-en 8894 df-dom 8895 df-sdom 8896

This theorem is referenced by: 0sdom 9046 fodomr 9066 pwdom 9067 0sdom1dom 9156 1sdom2dom 9164 infn0ALT 9213 fodomfir 9238 fodomfib 9239 fodomfibOLD 9241 domwdom 9489 iunfictbso 10036 djulepw 10115 fin45 10314 fodomb 10448 brdom3 10450 gchxpidm 10592 inar1 10698 csdfil 23859 ovoliunnul 25474 carsgclctunlem3 34464 domalom 37720 ovoliunnfl 37983 voliunnfl 37985 volsupnfl 37986 sdomne0 43840 sdomne0d 43841 ensucne0OLD 43957 nnfoctb 45479 caragenunicl 46952

W3C validator