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

Theorem elunii 4912
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 2830 . . . . 5 (𝑥 = 𝐵 → (𝐴𝑥𝐴𝐵))
2 eleq1 2829 . . . . 5 (𝑥 = 𝐵 → (𝑥𝐶𝐵𝐶))
31, 2anbi12d 632 . . . 4 (𝑥 = 𝐵 → ((𝐴𝑥𝑥𝐶) ↔ (𝐴𝐵𝐵𝐶)))
43spcegv 3597 . . 3 (𝐵𝐶 → ((𝐴𝐵𝐵𝐶) → ∃𝑥(𝐴𝑥𝑥𝐶)))
54anabsi7 671 . 2 ((𝐴𝐵𝐵𝐶) → ∃𝑥(𝐴𝑥𝑥𝐶))
6 eluni 4910 . 2 (𝐴 𝐶 ↔ ∃𝑥(𝐴𝑥𝑥𝐶))
75, 6sylibr 234 1 ((𝐴𝐵𝐵𝐶) → 𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  wex 1779  wcel 2108   cuni 4907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-uni 4908
This theorem is referenced by:  ssuni  4932  unipw  5455  opeluu  5475  unon  7851  limuni3  7873  naddsuc2  8739  uniinqs  8837  trcl  9768  rankwflemb  9833  ac5num  10076  dfac3  10161  isf34lem4  10417  axcclem  10497  ttukeylem7  10555  brdom7disj  10571  brdom6disj  10572  wrdexb  14563  dprdfeq0  20042  tgss2  22994  ppttop  23014  isclo  23095  neips  23121  2ndcomap  23466  2ndcsep  23467  locfincmp  23534  comppfsc  23540  txkgen  23660  txconn  23697  basqtop  23719  nrmr0reg  23757  alexsublem  24052  alexsubALTlem4  24058  alexsubALT  24059  ptcmplem4  24063  unirnblps  24429  unirnbl  24430  blbas  24440  met2ndci  24535  bndth  24990  dyadmbllem  25634  opnmbllem  25636  ssdifidllem  33484  ssmxidllem  33501  dya2iocnei  34284  dstfrvunirn  34477  pconnconn  35236  cvmcov2  35280  cvmlift2lem11  35318  cvmlift2lem12  35319  neibastop2lem  36361  onint1  36450  icoreunrn  37360  opnmbllem0  37663  heibor1  37817  unichnidl  38038  prtlem16  38870  prter2  38882  truniALT  44561  unipwrVD  44852  unipwr  44853  truniALTVD  44898  unisnALT  44946  restuni3  45123  disjinfi  45197  stoweidlem43  46058  stoweidlem55  46070  salexct  46349
  Copyright terms: Public domain W3C validator