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

Theorem elun 3112
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 2583 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 2583 . . 3 (𝐴𝐵𝐴 ∈ V)
3 elex 2583 . . 3 (𝐴𝐶𝐴 ∈ V)
42, 3jaoi 646 . 2 ((𝐴𝐵𝐴𝐶) → 𝐴 ∈ V)
5 eleq1 2116 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
6 eleq1 2116 . . . 4 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
75, 6orbi12d 717 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵𝑥𝐶) ↔ (𝐴𝐵𝐴𝐶)))
8 df-un 2950 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵𝑥𝐶)}
97, 8elab2g 2712 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶)))
101, 4, 9pm5.21nii 630 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff set class
Syntax hints:  wb 102  wo 639   = wceq 1259  wcel 1409  Vcvv 2574  cun 2943
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-v 2576  df-un 2950
This theorem is referenced by:  uneqri  3113  uncom  3115  uneq1  3118  unass  3128  ssun1  3134  unss1  3140  ssequn1  3141  unss  3145  rexun  3151  ralunb  3152  unssdif  3200  unssin  3204  inssun  3205  indi  3212  undi  3213  difundi  3217  difindiss  3219  undif3ss  3226  symdifxor  3231  rabun2  3244  reuun2  3248  undif4  3312  ssundifim  3334  dfpr2  3422  eltpg  3444  pwprss  3604  pwtpss  3605  uniun  3627  intun  3674  iunun  3762  iunxun  3763  iinuniss  3765  brun  3838  pwunss  4048  elsuci  4168  elsucg  4169  elsuc2g  4170  ordsucim  4254  sucprcreg  4301  opthprc  4419  xpundi  4424  xpundir  4425  funun  4972  mptun  5057  unpreima  5320  reldmtpos  5899  dftpos4  5909  tpostpos  5910  onunsnss  6386  elnn0  8241  un0addcl  8272  un0mulcl  8273  ltxr  8796  elxr  8797  fzsplit2  9016  elfzp1  9036  uzsplit  9056  elfzp12  9063  fzosplit  9135  fzouzsplit  9137  elfzonlteqm1  9168  fzosplitsni  9193  fz01or  10190  bj-nntrans  10463  bj-nnelirr  10465
  Copyright terms: Public domain W3C validator