Theorem rabeq0 3477

Description: Condition for a restricted class abstraction to be empty. (Contributed by Jeff Madsen, 7-Jun-2010.)

Assertion

Ref	Expression
rabeq0	⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

Proof of Theorem rabeq0

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		imnan 691	. . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝜑) ↔ ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2	1	albii 1481	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝜑) ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-ral 2477	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝜑))
4		sbn 1968	. . . 4 ⊢ ([𝑦 / 𝑥] ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ [𝑦 / 𝑥](𝑥 ∈ 𝐴 ∧ 𝜑))
5	4	albii 1481	. . 3 ⊢ (∀𝑦[𝑦 / 𝑥] ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∀𝑦 ¬ [𝑦 / 𝑥](𝑥 ∈ 𝐴 ∧ 𝜑))
6		nfv 1539	. . . 4 ⊢ Ⅎ𝑦 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑)
7	6	sb8 1867	. . 3 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∀𝑦[𝑦 / 𝑥] ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
8		eq0 3466	. . . 4 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})
9		df-rab 2481	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
10	9	eleq2i 2260	. . . . . . 7 ⊢ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)})
11		df-clab 2180	. . . . . . 7 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝐴 ∧ 𝜑))
12	10, 11	bitri 184	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝐴 ∧ 𝜑))
13	12	notbii 669	. . . . 5 ⊢ (¬ 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ¬ [𝑦 / 𝑥](𝑥 ∈ 𝐴 ∧ 𝜑))
14	13	albii 1481	. . . 4 ⊢ (∀𝑦 ¬ 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑦 ¬ [𝑦 / 𝑥](𝑥 ∈ 𝐴 ∧ 𝜑))
15	8, 14	bitri 184	. . 3 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑦 ¬ [𝑦 / 𝑥](𝑥 ∈ 𝐴 ∧ 𝜑))
16	5, 7, 15	3bitr4ri 213	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
17	2, 3, 16	3bitr4ri 213	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1362   = wceq 1364  [wsb 1773   ∈ wcel 2164  {cab 2179  ∀wral 2472  {crab 2476  ∅c0 3447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rab 2481  df-v 2762  df-dif 3156  df-nul 3448

This theorem is referenced by:  rabnc  3480  rabrsndc  3687  exmidsssnc  4233  ssfilem  6933  diffitest  6945  ssfirab  6992  ctssexmid  7211  exmidonfinlem  7255  iooidg  9978  icc0r  9995  fznlem  10110  ioo0  10331  ico0  10333  ioc0  10334  phiprmpw  12363  hashgcdeq  12380  unennn  12557  znnen  12558  fczpsrbag  14168  lgsquadlem2  15235