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

Theorem elun 3156
Description: Expansion of membership in class union. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 7-Aug-1994.)
Assertion
Ref Expression
elun (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))

Proof of Theorem elun
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 elex 2644 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 2644 . . 3 (𝐴𝐵𝐴 ∈ V)
3 elex 2644 . . 3 (𝐴𝐶𝐴 ∈ V)
42, 3jaoi 674 . 2 ((𝐴𝐵𝐴𝐶) → 𝐴 ∈ V)
5 eleq1 2157 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
6 eleq1 2157 . . . 4 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
75, 6orbi12d 745 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵𝑥𝐶) ↔ (𝐴𝐵𝐴𝐶)))
8 df-un 3017 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵𝑥𝐶)}
97, 8elab2g 2776 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶)))
101, 4, 9pm5.21nii 658 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff set class
Syntax hints:  wb 104  wo 667   = wceq 1296  wcel 1445  Vcvv 2633  cun 3011
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-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-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077
This theorem depends on definitions:  df-bi 116  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-v 2635  df-un 3017
This theorem is referenced by:  uneqri  3157  uncom  3159  uneq1  3162  unass  3172  ssun1  3178  unss1  3184  ssequn1  3185  unss  3189  rexun  3195  ralunb  3196  unssdif  3250  unssin  3254  inssun  3255  indi  3262  undi  3263  difundi  3267  difindiss  3269  undif3ss  3276  symdifxor  3281  rabun2  3294  reuun2  3298  undif4  3364  ssundifim  3385  dcun  3412  dfpr2  3485  eltpg  3508  pwprss  3671  pwtpss  3672  uniun  3694  intun  3741  iunun  3830  iunxun  3831  iinuniss  3833  brun  3913  undifexmid  4049  exmidundif  4058  exmidundifim  4059  pwunss  4134  elsuci  4254  elsucg  4255  elsuc2g  4256  ordsucim  4345  sucprcreg  4393  opthprc  4518  xpundi  4523  xpundir  4524  funun  5092  mptun  5178  unpreima  5463  reldmtpos  6056  dftpos4  6066  tpostpos  6067  onunsnss  6707  unfidisj  6712  undifdcss  6713  fidcenumlemrks  6742  djulclb  6827  djur  6837  eldju  6839  djuun  6840  eldju2ndl  6843  eldju2ndr  6844  elnn0  8773  un0addcl  8804  un0mulcl  8805  elxnn0  8836  ltxr  9345  elxr  9346  fzsplit2  9613  elfzp1  9635  uzsplit  9655  elfzp12  9662  fz01or  9674  fzosplit  9737  fzouzsplit  9739  elfzonlteqm1  9770  fzosplitsni  9795  hashinfuni  10300  hashennnuni  10302  hashunlem  10327  zfz1isolemiso  10359  summodclem3  10923  fsumsplit  10950  fsumsplitsn  10953  sumsplitdc  10975  djulclALT  12409  djurclALT  12410  bj-nntrans  12554  bj-nnelirr  12556
  Copyright terms: Public domain W3C validator