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 9041

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

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

**Proof of Theorem 0sdomg**
Step	Hyp	Ref	Expression
1		0domg 9039	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∅ ≼ 𝐴)
2		brsdom 8918	. . . 4 ⊢ (∅ ≺ 𝐴 ↔ (∅ ≼ 𝐴 ∧ ¬ ∅ ≈ 𝐴))
3	2	baib 540	. . 3 ⊢ (∅ ≼ 𝐴 → (∅ ≺ 𝐴 ↔ ¬ ∅ ≈ 𝐴))
4	1, 3	syl 17	. 2 ⊢ (𝐴 ∈ 𝑉 → (∅ ≺ 𝐴 ↔ ¬ ∅ ≈ 𝐴))
5		en0r 8964	. . 3 ⊢ (∅ ≈ 𝐴 ↔ 𝐴 = ∅)
6	5	necon3bbii 2982	. 2 ⊢ (¬ ∅ ≈ 𝐴 ↔ 𝐴 ≠ ∅)
7	4, 6	bitrdi 288	1 ⊢ (𝐴 ∈ 𝑉 → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∈ wcel 2119 ≠ wne 2935 ∅c0 4268 class class class wbr 5079 ≈ cen 8887 ≼ cdom 8888 ≺ csdm 8889

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-ext 2712 ax-sep 5225 ax-nul 5235 ax-pr 5369

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-sb 2074 df-mo 2543 df-clab 2719 df-cleq 2732 df-clel 2815 df-ne 2936 df-ral 3055 df-rex 3065 df-rab 3393 df-v 3434 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4269 df-if 4462 df-sn 4563 df-pr 4565 df-op 4569 df-br 5080 df-opab 5142 df-id 5520 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-en 8891 df-dom 8892 df-sdom 8893

This theorem is referenced by: 0sdom 9043 fodomr 9063 pwdom 9064 0sdom1dom 9153 1sdom2dom 9161 infn0ALT 9210 fodomfir 9235 fodomfib 9236 fodomfibOLD 9238 domwdom 9486 iunfictbso 10034 djulepw 10113 fin45 10312 fodomb 10446 brdom3 10448 gchxpidm 10590 inar1 10696 csdfil 23884 ovoliunnul 25499 carsgclctunlem3 34511 domalom 37773 ovoliunnfl 38036 voliunnfl 38038 volsupnfl 38039 sdomne0 43864 sdomne0d 43865 ensucne0OLD 43981 nnfoctb 45503 caragenunicl 46974

W3C validator