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

Theorem abnex 4297
Description: Sufficient condition for a class abstraction to be a proper class. Lemma for snnex 4298 and pwnex 4299. See the comment of abnexg 4296. (Contributed by BJ, 2-May-2021.)
Assertion
Ref Expression
abnex (∀𝑥(𝐹𝑉𝑥𝐹) → ¬ {𝑦 ∣ ∃𝑥 𝑦 = 𝐹} ∈ V)
Distinct variable groups:   𝑥,𝑦   𝑦,𝐹
Allowed substitution hints:   𝐹(𝑥)   𝑉(𝑥,𝑦)

Proof of Theorem abnex
StepHypRef Expression
1 vprc 3992 . 2 ¬ V ∈ V
2 alral 2432 . . 3 (∀𝑥(𝐹𝑉𝑥𝐹) → ∀𝑥 ∈ V (𝐹𝑉𝑥𝐹))
3 rexv 2651 . . . . . . 7 (∃𝑥 ∈ V 𝑦 = 𝐹 ↔ ∃𝑥 𝑦 = 𝐹)
43bicomi 131 . . . . . 6 (∃𝑥 𝑦 = 𝐹 ↔ ∃𝑥 ∈ V 𝑦 = 𝐹)
54abbii 2210 . . . . 5 {𝑦 ∣ ∃𝑥 𝑦 = 𝐹} = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = 𝐹}
65eleq1i 2160 . . . 4 ({𝑦 ∣ ∃𝑥 𝑦 = 𝐹} ∈ V ↔ {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = 𝐹} ∈ V)
76biimpi 119 . . 3 ({𝑦 ∣ ∃𝑥 𝑦 = 𝐹} ∈ V → {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = 𝐹} ∈ V)
8 abnexg 4296 . . 3 (∀𝑥 ∈ V (𝐹𝑉𝑥𝐹) → ({𝑦 ∣ ∃𝑥 ∈ V 𝑦 = 𝐹} ∈ V → V ∈ V))
92, 7, 8syl2im 38 . 2 (∀𝑥(𝐹𝑉𝑥𝐹) → ({𝑦 ∣ ∃𝑥 𝑦 = 𝐹} ∈ V → V ∈ V))
101, 9mtoi 628 1 (∀𝑥(𝐹𝑉𝑥𝐹) → ¬ {𝑦 ∣ ∃𝑥 𝑦 = 𝐹} ∈ V)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wal 1294   = wceq 1296  wex 1433  wcel 1445  {cab 2081  wral 2370  wrex 2371  Vcvv 2633
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-13 1456  ax-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-sep 3978  ax-un 4284
This theorem depends on definitions:  df-bi 116  df-tru 1299  df-fal 1302  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ral 2375  df-rex 2376  df-v 2635  df-in 3019  df-ss 3026  df-sn 3472  df-uni 3676  df-iun 3754
This theorem is referenced by:  pwnex  4299
  Copyright terms: Public domain W3C validator