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 9037

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

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

**Proof of Theorem 0sdomg**
Step	Hyp	Ref	Expression
1		0domg 9035	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∅ ≼ 𝐴)
2		brsdom 8914	. . . 4 ⊢ (∅ ≺ 𝐴 ↔ (∅ ≼ 𝐴 ∧ ¬ ∅ ≈ 𝐴))
3	2	baib 535	. . 3 ⊢ (∅ ≼ 𝐴 → (∅ ≺ 𝐴 ↔ ¬ ∅ ≈ 𝐴))
4	1, 3	syl 17	. 2 ⊢ (𝐴 ∈ 𝑉 → (∅ ≺ 𝐴 ↔ ¬ ∅ ≈ 𝐴))
5		en0r 8960	. . 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 4274 class class class wbr 5086 ≈ cen 8883 ≼ cdom 8884 ≺ csdm 8885

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 5231 ax-nul 5241 ax-pr 5370

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 3391 df-v 3432 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-sn 4569 df-pr 4571 df-op 4575 df-br 5087 df-opab 5149 df-id 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-en 8887 df-dom 8888 df-sdom 8889

This theorem is referenced by: 0sdom 9039 fodomr 9059 pwdom 9060 0sdom1dom 9149 1sdom2dom 9157 infn0ALT 9206 fodomfir 9231 fodomfib 9232 fodomfibOLD 9234 domwdom 9482 iunfictbso 10027 djulepw 10106 fin45 10305 fodomb 10439 brdom3 10441 gchxpidm 10583 inar1 10689 csdfil 23869 ovoliunnul 25484 carsgclctunlem3 34480 domalom 37734 ovoliunnfl 37997 voliunnfl 37999 volsupnfl 38000 sdomne0 43858 sdomne0d 43859 ensucne0OLD 43975 nnfoctb 45497 caragenunicl 46970

W3C validator