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 9046

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

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

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

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∈ wcel 2114 ≠ wne 2933 ∅c0 4287 class class class wbr 5100 ≈ cen 8892 ≼ cdom 8893 ≺ csdm 8894

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 2709 ax-sep 5243 ax-nul 5253 ax-pr 5379

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 2540 df-clab 2716 df-cleq 2729 df-clel 2812 df-ne 2934 df-ral 3053 df-rex 3063 df-rab 3402 df-v 3444 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4288 df-if 4482 df-sn 4583 df-pr 4585 df-op 4589 df-br 5101 df-opab 5163 df-id 5527 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-en 8896 df-dom 8897 df-sdom 8898

This theorem is referenced by: 0sdom 9048 fodomr 9068 pwdom 9069 0sdom1dom 9158 1sdom2dom 9166 infn0ALT 9215 fodomfir 9240 fodomfib 9241 fodomfibOLD 9243 domwdom 9491 iunfictbso 10036 djulepw 10115 fin45 10314 fodomb 10448 brdom3 10450 gchxpidm 10592 inar1 10698 csdfil 23850 ovoliunnul 25476 carsgclctunlem3 34497 domalom 37653 ovoliunnfl 37907 voliunnfl 37909 volsupnfl 37910 sdomne0 43763 sdomne0d 43764 ensucne0OLD 43880 nnfoctb 45402 caragenunicl 46876

W3C validator