Theorem dif1o 8124

Description: Two ways to say that 𝐴 is a nonzero number of the set 𝐵. (Contributed by Mario Carneiro, 21-May-2015.)

Assertion

Ref	Expression
dif1o	⊢ (𝐴 ∈ (𝐵 ∖ 1o) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅))

Proof of Theorem dif1o

Step	Hyp	Ref	Expression
1		df1o2 8115	. . . 4 ⊢ 1o = {∅}
2	1	difeq2i 4095	. . 3 ⊢ (𝐵 ∖ 1o) = (𝐵 ∖ {∅})
3	2	eleq2i 2904	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 1o) ↔ 𝐴 ∈ (𝐵 ∖ {∅}))
4		eldifsn 4718	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {∅}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅))
5	3, 4	bitri 277	1 ⊢ (𝐴 ∈ (𝐵 ∖ 1o) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅))

Syntax hints:   ↔ wb 208   ∧ wa 398   ∈ wcel 2110   ≠ wne 3016   ∖ cdif 3932  ∅c0 4290  {csn 4566  1_oc1o 8094

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-nul 4291  df-sn 4567  df-suc 6196  df-1o 8101

This theorem is referenced by:  ondif1  8125  brwitnlem  8131  oelim2  8220  oeeulem  8226  oeeui  8227  omabs  8273  cantnfp1lem3  9142  cantnfp1  9143  cantnflem1  9151  cantnflem3  9153  cantnflem4  9154  cnfcom3lem  9165