MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elunii Structured version   Visualization version   GIF version

Theorem elunii 4367
Description: Membership in class union. (Contributed by NM, 24-Mar-1995.)
Assertion
Ref Expression
elunii ((𝐴𝐵𝐵𝐶) → 𝐴 𝐶)

Proof of Theorem elunii
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 eleq2 2672 . . . . 5 (𝑥 = 𝐵 → (𝐴𝑥𝐴𝐵))
2 eleq1 2671 . . . . 5 (𝑥 = 𝐵 → (𝑥𝐶𝐵𝐶))
31, 2anbi12d 742 . . . 4 (𝑥 = 𝐵 → ((𝐴𝑥𝑥𝐶) ↔ (𝐴𝐵𝐵𝐶)))
43spcegv 3262 . . 3 (𝐵𝐶 → ((𝐴𝐵𝐵𝐶) → ∃𝑥(𝐴𝑥𝑥𝐶)))
54anabsi7 855 . 2 ((𝐴𝐵𝐵𝐶) → ∃𝑥(𝐴𝑥𝑥𝐶))
6 eluni 4365 . 2 (𝐴 𝐶 ↔ ∃𝑥(𝐴𝑥𝑥𝐶))
75, 6sylibr 222 1 ((𝐴𝐵𝐵𝐶) → 𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wex 1694  wcel 1975   cuni 4362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-v 3170  df-uni 4363
This theorem is referenced by:  ssuni  4385  ssuniOLD  4386  unipw  4835  opeluu  4856  unon  6896  limuni3  6917  uniinqs  7687  trcl  8460  rankwflemb  8512  ac5num  8715  dfac3  8800  isf34lem4  9055  axcclem  9135  ttukeylem7  9193  brdom7disj  9207  brdom6disj  9208  wrdexb  13113  dprdfeq0  18186  tgss2  20540  ppttop  20559  isclo  20639  neips  20665  2ndcomap  21009  2ndcsep  21010  locfincmp  21077  comppfsc  21083  txkgen  21203  txcon  21240  basqtop  21262  nrmr0reg  21300  alexsublem  21596  alexsubALTlem4  21602  alexsubALT  21603  ptcmplem4  21607  unirnblps  21971  unirnbl  21972  blbas  21982  met2ndci  22074  bndth  22492  dyadmbllem  23086  opnmbllem  23088  dya2iocnei  29473  dstfrvunirn  29665  pconcon  30269  cvmcov2  30313  cvmlift2lem11  30351  cvmlift2lem12  30352  neibastop2lem  31327  onint1  31420  icoreunrn  32182  opnmbllem0  32414  heibor1  32578  unichnidl  32799  prtlem16  32971  prter2  32983  truniALT  37571  unipwrVD  37888  unipwr  37889  truniALTVD  37935  unisnALT  37983  restuni3  38132  disjinfi  38174  stoweidlem43  38736  stoweidlem55  38748  salexct  39028
  Copyright terms: Public domain W3C validator