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

Theorem elunii 4377
 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 2677 . . . . 5 (𝑥 = 𝐵 → (𝐴𝑥𝐴𝐵))
2 eleq1 2676 . . . . 5 (𝑥 = 𝐵 → (𝑥𝐶𝐵𝐶))
31, 2anbi12d 743 . . . 4 (𝑥 = 𝐵 → ((𝐴𝑥𝑥𝐶) ↔ (𝐴𝐵𝐵𝐶)))
43spcegv 3267 . . 3 (𝐵𝐶 → ((𝐴𝐵𝐵𝐶) → ∃𝑥(𝐴𝑥𝑥𝐶)))
54anabsi7 856 . 2 ((𝐴𝐵𝐵𝐶) → ∃𝑥(𝐴𝑥𝑥𝐶))
6 eluni 4375 . 2 (𝐴 𝐶 ↔ ∃𝑥(𝐴𝑥𝑥𝐶))
75, 6sylibr 223 1 ((𝐴𝐵𝐵𝐶) → 𝐴 𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475  ∃wex 1695   ∈ wcel 1977  ∪ cuni 4372 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-uni 4373 This theorem is referenced by:  ssuni  4395  ssuniOLD  4396  unipw  4845  opeluu  4866  unon  6923  limuni3  6944  uniinqs  7714  trcl  8487  rankwflemb  8539  ac5num  8742  dfac3  8827  isf34lem4  9082  axcclem  9162  ttukeylem7  9220  brdom7disj  9234  brdom6disj  9235  wrdexb  13171  dprdfeq0  18244  tgss2  20602  ppttop  20621  isclo  20701  neips  20727  2ndcomap  21071  2ndcsep  21072  locfincmp  21139  comppfsc  21145  txkgen  21265  txcon  21302  basqtop  21324  nrmr0reg  21362  alexsublem  21658  alexsubALTlem4  21664  alexsubALT  21665  ptcmplem4  21669  unirnblps  22034  unirnbl  22035  blbas  22045  met2ndci  22137  bndth  22565  dyadmbllem  23173  opnmbllem  23175  dya2iocnei  29671  dstfrvunirn  29863  pconcon  30467  cvmcov2  30511  cvmlift2lem11  30549  cvmlift2lem12  30550  neibastop2lem  31525  onint1  31618  icoreunrn  32383  opnmbllem0  32615  heibor1  32779  unichnidl  33000  prtlem16  33172  prter2  33184  truniALT  37772  unipwrVD  38089  unipwr  38090  truniALTVD  38136  unisnALT  38184  restuni3  38333  disjinfi  38375  stoweidlem43  38936  stoweidlem55  38948  salexct  39228
 Copyright terms: Public domain W3C validator