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 9074

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

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

**Proof of Theorem 0sdomg**
Step	Hyp	Ref	Expression
1		0domg 9072	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∅ ≼ 𝐴)
2		brsdom 8951	. . . 4 ⊢ (∅ ≺ 𝐴 ↔ (∅ ≼ 𝐴 ∧ ¬ ∅ ≈ 𝐴))
3	2	baib 543	. . 3 ⊢ (∅ ≼ 𝐴 → (∅ ≺ 𝐴 ↔ ¬ ∅ ≈ 𝐴))
4	1, 3	syl 17	. 2 ⊢ (𝐴 ∈ 𝑉 → (∅ ≺ 𝐴 ↔ ¬ ∅ ≈ 𝐴))
5		en0r 8997	. . 3 ⊢ (∅ ≈ 𝐴 ↔ 𝐴 = ∅)
6	5	necon3bbii 3003	. 2 ⊢ (¬ ∅ ≈ 𝐴 ↔ 𝐴 ≠ ∅)
7	4, 6	bitrdi 289	1 ⊢ (𝐴 ∈ 𝑉 → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∈ wcel 2141 ≠ wne 2956 ∅c0 4285 class class class wbr 5099 ≈ cen 8920 ≼ cdom 8921 ≺ csdm 8922

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-ext 2733 ax-sep 5245 ax-nul 5255 ax-pr 5389

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-sb 2090 df-mo 2565 df-clab 2740 df-cleq 2753 df-clel 2836 df-ne 2957 df-ral 3076 df-rex 3086 df-rab 3414 df-v 3455 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-nul 4286 df-if 4480 df-sn 4582 df-pr 4584 df-op 4588 df-br 5100 df-opab 5162 df-id 5540 df-xp 5651 df-rel 5652 df-cnv 5653 df-co 5654 df-dm 5655 df-rn 5656 df-fun 6519 df-fn 6520 df-f 6521 df-f1 6522 df-fo 6523 df-f1o 6524 df-en 8924 df-dom 8925 df-sdom 8926

This theorem is referenced by: 0sdom 9076 fodomr 9096 pwdom 9097 0sdom1dom 9186 1sdom2dom 9194 infn0ALT 9243 fodomfir 9268 fodomfib 9269 fodomfibOLD 9271 domwdom 9519 iunfictbso 10067 djulepw 10146 fin45 10346 fodomb 10480 brdom3 10482 gchxpidm 10624 inar1 10730 csdfil 23934 ovoliunnul 25549 carsgclctunlem3 34578 domalom 37862 ovoliunnfl 38125 voliunnfl 38127 volsupnfl 38128 sdomne0 43953 sdomne0d 43954 ensucne0OLD 44070 nnfoctb 45592 caragenunicl 47062

W3C validator