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

Theorem elun 3261
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 2735 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 2735 . . 3 (𝐴𝐵𝐴 ∈ V)
3 elex 2735 . . 3 (𝐴𝐶𝐴 ∈ V)
42, 3jaoi 706 . 2 ((𝐴𝐵𝐴𝐶) → 𝐴 ∈ V)
5 eleq1 2227 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
6 eleq1 2227 . . . 4 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
75, 6orbi12d 783 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵𝑥𝐶) ↔ (𝐴𝐵𝐴𝐶)))
8 df-un 3118 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵𝑥𝐶)}
97, 8elab2g 2871 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶)))
101, 4, 9pm5.21nii 694 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff set class
Syntax hints:  wb 104  wo 698   = wceq 1342  wcel 2135  Vcvv 2724  cun 3112
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-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146
This theorem depends on definitions:  df-bi 116  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-v 2726  df-un 3118
This theorem is referenced by:  uneqri  3262  uncom  3264  uneq1  3267  unass  3277  ssun1  3283  unss1  3289  ssequn1  3290  unss  3294  rexun  3300  ralunb  3301  unssdif  3355  unssin  3359  inssun  3360  indi  3367  undi  3368  difundi  3372  difindiss  3374  undif3ss  3381  symdifxor  3386  rabun2  3399  reuun2  3403  undif4  3469  ssundifim  3490  dcun  3517  dfpr2  3592  eltpg  3618  pwprss  3782  pwtpss  3783  uniun  3805  intun  3852  iunun  3941  iunxun  3942  iinuniss  3945  brun  4030  undifexmid  4169  exmidundif  4182  exmidundifim  4183  pwunss  4258  elsuci  4378  elsucg  4379  elsuc2g  4380  ordsucim  4474  sucprcreg  4523  opthprc  4652  xpundi  4657  xpundir  4658  funun  5229  mptun  5316  unpreima  5607  reldmtpos  6215  dftpos4  6225  tpostpos  6226  onunsnss  6876  unfidisj  6881  undifdcss  6882  fidcenumlemrks  6912  djulclb  7014  eldju  7027  eldju2ndl  7031  eldju2ndr  7032  ctssdccl  7070  pw1nel3  7181  sucpw1nel3  7183  elnn0  9110  un0addcl  9141  un0mulcl  9142  elxnn0  9173  ltxr  9705  elxr  9706  fzsplit2  9979  elfzp1  10001  uzsplit  10021  elfzp12  10028  fz01or  10040  fzosplit  10106  fzouzsplit  10108  elfzonlteqm1  10139  fzosplitsni  10164  hashinfuni  10684  hashennnuni  10686  hashunlem  10711  zfz1isolemiso  10746  summodclem3  11315  fsumsplit  11342  fsumsplitsn  11345  sumsplitdc  11367  fprodsplitdc  11531  fprodsplit  11532  fprodunsn  11539  fprodsplitsn  11568  nnnn0modprm0  12181  prm23lt5  12189  reopnap  13136  djulclALT  13575  djurclALT  13576  bj-charfun  13582  bj-nntrans  13726  bj-nnelirr  13728  exmid1stab  13773
  Copyright terms: Public domain W3C validator