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

Theorem elun 3084
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 2566 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 2566 . . 3 (𝐴𝐵𝐴 ∈ V)
3 elex 2566 . . 3 (𝐴𝐶𝐴 ∈ V)
42, 3jaoi 636 . 2 ((𝐴𝐵𝐴𝐶) → 𝐴 ∈ V)
5 eleq1 2100 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
6 eleq1 2100 . . . 4 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
75, 6orbi12d 707 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵𝑥𝐶) ↔ (𝐴𝐵𝐴𝐶)))
8 df-un 2922 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵𝑥𝐶)}
97, 8elab2g 2689 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶)))
101, 4, 9pm5.21nii 620 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff set class
Syntax hints:  wb 98  wo 629   = wceq 1243  wcel 1393  Vcvv 2557  cun 2915
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-v 2559  df-un 2922
This theorem is referenced by:  uneqri  3085  uncom  3087  uneq1  3090  unass  3100  ssun1  3106  unss1  3112  ssequn1  3113  unss  3117  rexun  3123  ralunb  3124  unssdif  3172  unssin  3176  inssun  3177  indi  3184  undi  3185  difundi  3189  difindiss  3191  undif3ss  3198  symdifxor  3203  rabun2  3216  reuun2  3220  undif4  3284  ssundifim  3306  dfpr2  3394  eltpg  3416  pwprss  3576  pwtpss  3577  uniun  3599  intun  3646  iunun  3734  iunxun  3735  iinuniss  3737  brun  3810  pwunss  4020  elsuci  4140  elsucg  4141  elsuc2g  4142  ordsucim  4226  sucprcreg  4273  opthprc  4391  xpundi  4396  xpundir  4397  funun  4944  mptun  5029  unpreima  5292  reldmtpos  5868  dftpos4  5878  tpostpos  5879  elnn0  8181  un0addcl  8213  un0mulcl  8214  ltxr  8693  elxr  8694  fzsplit2  8912  elfzp1  8932  uzsplit  8952  elfzp12  8959  fzosplit  9031  fzouzsplit  9033  elfzonlteqm1  9064  fzosplitsni  9089  bj-nntrans  10050  bj-nnelirr  10052
  Copyright terms: Public domain W3C validator