Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  rabeq0 GIF version

Theorem rabeq0 3419
 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.
StepHypRef Expression
1 imnan 680 . . 3 ((𝑥𝐴 → ¬ 𝜑) ↔ ¬ (𝑥𝐴𝜑))
21albii 1447 . 2 (∀𝑥(𝑥𝐴 → ¬ 𝜑) ↔ ∀𝑥 ¬ (𝑥𝐴𝜑))
3 df-ral 2437 . 2 (∀𝑥𝐴 ¬ 𝜑 ↔ ∀𝑥(𝑥𝐴 → ¬ 𝜑))
4 sbn 1929 . . . 4 ([𝑦 / 𝑥] ¬ (𝑥𝐴𝜑) ↔ ¬ [𝑦 / 𝑥](𝑥𝐴𝜑))
54albii 1447 . . 3 (∀𝑦[𝑦 / 𝑥] ¬ (𝑥𝐴𝜑) ↔ ∀𝑦 ¬ [𝑦 / 𝑥](𝑥𝐴𝜑))
6 nfv 1505 . . . 4 𝑦 ¬ (𝑥𝐴𝜑)
76sb8 1833 . . 3 (∀𝑥 ¬ (𝑥𝐴𝜑) ↔ ∀𝑦[𝑦 / 𝑥] ¬ (𝑥𝐴𝜑))
8 eq0 3408 . . . 4 ({𝑥𝐴𝜑} = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ {𝑥𝐴𝜑})
9 df-rab 2441 . . . . . . . 8 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
109eleq2i 2221 . . . . . . 7 (𝑦 ∈ {𝑥𝐴𝜑} ↔ 𝑦 ∈ {𝑥 ∣ (𝑥𝐴𝜑)})
11 df-clab 2141 . . . . . . 7 (𝑦 ∈ {𝑥 ∣ (𝑥𝐴𝜑)} ↔ [𝑦 / 𝑥](𝑥𝐴𝜑))
1210, 11bitri 183 . . . . . 6 (𝑦 ∈ {𝑥𝐴𝜑} ↔ [𝑦 / 𝑥](𝑥𝐴𝜑))
1312notbii 658 . . . . 5 𝑦 ∈ {𝑥𝐴𝜑} ↔ ¬ [𝑦 / 𝑥](𝑥𝐴𝜑))
1413albii 1447 . . . 4 (∀𝑦 ¬ 𝑦 ∈ {𝑥𝐴𝜑} ↔ ∀𝑦 ¬ [𝑦 / 𝑥](𝑥𝐴𝜑))
158, 14bitri 183 . . 3 ({𝑥𝐴𝜑} = ∅ ↔ ∀𝑦 ¬ [𝑦 / 𝑥](𝑥𝐴𝜑))
165, 7, 153bitr4ri 212 . 2 ({𝑥𝐴𝜑} = ∅ ↔ ∀𝑥 ¬ (𝑥𝐴𝜑))
172, 3, 163bitr4ri 212 1 ({𝑥𝐴𝜑} = ∅ ↔ ∀𝑥𝐴 ¬ 𝜑)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104  ∀wal 1330   = wceq 1332  [wsb 1739   ∈ wcel 2125  {cab 2140  ∀wral 2432  {crab 2436  ∅c0 3390 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-ext 2136 This theorem depends on definitions:  df-bi 116  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1740  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-ral 2437  df-rab 2441  df-v 2711  df-dif 3100  df-nul 3391 This theorem is referenced by:  rabnc  3422  rabrsndc  3623  exmidsssnc  4159  ssfilem  6809  diffitest  6821  ssfirab  6867  ctssexmid  7072  exmidonfinlem  7107  iooidg  9791  icc0r  9808  fznlem  9921  ioo0  10137  ico0  10139  ioc0  10140  phiprmpw  12065  hashgcdeq  12071  unennn  12077  znnen  12078
 Copyright terms: Public domain W3C validator