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

Theorem elunii 4806
 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 2878 . . . . 5 (𝑥 = 𝐵 → (𝐴𝑥𝐴𝐵))
2 eleq1 2877 . . . . 5 (𝑥 = 𝐵 → (𝑥𝐶𝐵𝐶))
31, 2anbi12d 633 . . . 4 (𝑥 = 𝐵 → ((𝐴𝑥𝑥𝐶) ↔ (𝐴𝐵𝐵𝐶)))
43spcegv 3545 . . 3 (𝐵𝐶 → ((𝐴𝐵𝐵𝐶) → ∃𝑥(𝐴𝑥𝑥𝐶)))
54anabsi7 670 . 2 ((𝐴𝐵𝐵𝐶) → ∃𝑥(𝐴𝑥𝑥𝐶))
6 eluni 4804 . 2 (𝐴 𝐶 ↔ ∃𝑥(𝐴𝑥𝑥𝐶))
75, 6sylibr 237 1 ((𝐴𝐵𝐵𝐶) → 𝐴 𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∪ cuni 4801 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-uni 4802 This theorem is referenced by:  ssuni  4826  unipw  5309  opeluu  5328  unon  7533  limuni3  7554  uniinqs  8367  trcl  9161  rankwflemb  9213  ac5num  9454  dfac3  9539  isf34lem4  9795  axcclem  9875  ttukeylem7  9933  brdom7disj  9949  brdom6disj  9950  wrdexb  13875  dprdfeq0  19145  tgss2  21606  ppttop  21626  isclo  21706  neips  21732  2ndcomap  22077  2ndcsep  22078  locfincmp  22145  comppfsc  22151  txkgen  22271  txconn  22308  basqtop  22330  nrmr0reg  22368  alexsublem  22663  alexsubALTlem4  22669  alexsubALT  22670  ptcmplem4  22674  unirnblps  23040  unirnbl  23041  blbas  23051  met2ndci  23143  bndth  23577  dyadmbllem  24217  opnmbllem  24219  ssmxidllem  31080  dya2iocnei  31686  dstfrvunirn  31878  pconnconn  32627  cvmcov2  32671  cvmlift2lem11  32709  cvmlift2lem12  32710  neibastop2lem  33857  onint1  33946  icoreunrn  34816  opnmbllem0  35133  heibor1  35288  unichnidl  35509  prtlem16  36205  prter2  36217  truniALT  41311  unipwrVD  41602  unipwr  41603  truniALTVD  41648  unisnALT  41696  restuni3  41817  disjinfi  41883  stoweidlem43  42746  stoweidlem55  42758  salexct  43035
 Copyright terms: Public domain W3C validator