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

Theorem eluni 3549
 Description: Membership in class union. (Contributed by NM, 22-May-1994.)
Assertion
Ref Expression
eluni (A Bx(A x x B))
Distinct variable groups:   x,A   x,B

Proof of Theorem eluni
Dummy variable y is distinct from all other variables.
StepHypRef Expression
1 elex 2537 . 2 (A BA V)
2 elex 2537 . . . 4 (A xA V)
32adantr 261 . . 3 ((A x x B) → A V)
43exlimiv 1465 . 2 (x(A x x B) → A V)
5 eleq1 2076 . . . . 5 (y = A → (y xA x))
65anbi1d 438 . . . 4 (y = A → ((y x x B) ↔ (A x x B)))
76exbidv 1682 . . 3 (y = A → (x(y x x B) ↔ x(A x x B)))
8 df-uni 3547 . . 3 B = {yx(y x x B)}
97, 8elab2g 2660 . 2 (A V → (A Bx(A x x B)))
101, 4, 9pm5.21nii 604 1 (A Bx(A x x B))
 Colors of variables: wff set class Syntax hints:   ∧ wa 97   ↔ wb 98   = wceq 1226  ∃wex 1357   ∈ wcel 1369  Vcvv 2529  ∪ cuni 3546 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 614  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1358  ax-ie2 1359  ax-8 1371  ax-10 1372  ax-11 1373  ax-i12 1374  ax-bnd 1375  ax-4 1376  ax-17 1395  ax-i9 1399  ax-ial 1403  ax-i5r 1404  ax-ext 1998 This theorem depends on definitions:  df-bi 110  df-tru 1229  df-nf 1326  df-sb 1622  df-clab 2003  df-cleq 2009  df-clel 2012  df-nfc 2143  df-v 2531  df-uni 3547 This theorem is referenced by:  eluni2  3550  elunii  3551  eluniab  3558  uniun  3565  uniin  3566  uniss  3567  unissb  3576  dftr2  3822  unidif0  3886  unipw  3919  uniex2  4114  uniuni  4124  limom  4254  dmuni  4463  fununi  4884  nfvres  5122  elunirn  5321  tfrlem7  5846  tfrexlem  5861  bj-uniex2  8489
 Copyright terms: Public domain W3C validator