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 9034

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

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

**Proof of Theorem 0sdomg**
Step	Hyp	Ref	Expression
1		0domg 9032	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∅ ≼ 𝐴)
2		brsdom 8911	. . . 4 ⊢ (∅ ≺ 𝐴 ↔ (∅ ≼ 𝐴 ∧ ¬ ∅ ≈ 𝐴))
3	2	baib 535	. . 3 ⊢ (∅ ≼ 𝐴 → (∅ ≺ 𝐴 ↔ ¬ ∅ ≈ 𝐴))
4	1, 3	syl 17	. 2 ⊢ (𝐴 ∈ 𝑉 → (∅ ≺ 𝐴 ↔ ¬ ∅ ≈ 𝐴))
5		en0r 8957	. . 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 2113 ≠ wne 2932 ∅c0 4285 class class class wbr 5098 ≈ cen 8880 ≼ cdom 8881 ≺ csdm 8882

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 2708 ax-sep 5241 ax-nul 5251 ax-pr 5377

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 2539 df-clab 2715 df-cleq 2728 df-clel 2811 df-ne 2933 df-ral 3052 df-rex 3061 df-rab 3400 df-v 3442 df-dif 3904 df-un 3906 df-ss 3918 df-nul 4286 df-if 4480 df-sn 4581 df-pr 4583 df-op 4587 df-br 5099 df-opab 5161 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 8884 df-dom 8885 df-sdom 8886

This theorem is referenced by: 0sdom 9036 fodomr 9056 pwdom 9057 0sdom1dom 9146 1sdom2dom 9154 infn0ALT 9203 fodomfir 9228 fodomfib 9229 fodomfibOLD 9231 domwdom 9479 iunfictbso 10024 djulepw 10103 fin45 10302 fodomb 10436 brdom3 10438 gchxpidm 10580 inar1 10686 csdfil 23838 ovoliunnul 25464 carsgclctunlem3 34477 domalom 37605 ovoliunnfl 37859 voliunnfl 37861 volsupnfl 37862 sdomne0 43650 sdomne0d 43651 ensucne0OLD 43767 nnfoctb 45289 caragenunicl 46764

W3C validator