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

Theorem elunii 4593
 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 2828 . . . . 5 (𝑥 = 𝐵 → (𝐴𝑥𝐴𝐵))
2 eleq1 2827 . . . . 5 (𝑥 = 𝐵 → (𝑥𝐶𝐵𝐶))
31, 2anbi12d 749 . . . 4 (𝑥 = 𝐵 → ((𝐴𝑥𝑥𝐶) ↔ (𝐴𝐵𝐵𝐶)))
43spcegv 3434 . . 3 (𝐵𝐶 → ((𝐴𝐵𝐵𝐶) → ∃𝑥(𝐴𝑥𝑥𝐶)))
54anabsi7 895 . 2 ((𝐴𝐵𝐵𝐶) → ∃𝑥(𝐴𝑥𝑥𝐶))
6 eluni 4591 . 2 (𝐴 𝐶 ↔ ∃𝑥(𝐴𝑥𝑥𝐶))
75, 6sylibr 224 1 ((𝐴𝐵𝐵𝐶) → 𝐴 𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1632  ∃wex 1853   ∈ wcel 2139  ∪ cuni 4588 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-uni 4589 This theorem is referenced by:  ssuni  4611  ssuniOLD  4612  unipw  5067  opeluu  5087  unon  7196  limuni3  7217  uniinqs  7994  trcl  8777  rankwflemb  8829  ac5num  9049  dfac3  9134  isf34lem4  9391  axcclem  9471  ttukeylem7  9529  brdom7disj  9545  brdom6disj  9546  wrdexb  13502  dprdfeq0  18621  tgss2  20993  ppttop  21013  isclo  21093  neips  21119  2ndcomap  21463  2ndcsep  21464  locfincmp  21531  comppfsc  21537  txkgen  21657  txconn  21694  basqtop  21716  nrmr0reg  21754  alexsublem  22049  alexsubALTlem4  22055  alexsubALT  22056  ptcmplem4  22060  unirnblps  22425  unirnbl  22426  blbas  22436  met2ndci  22528  bndth  22958  dyadmbllem  23567  opnmbllem  23569  dya2iocnei  30653  dstfrvunirn  30845  pconnconn  31520  cvmcov2  31564  cvmlift2lem11  31602  cvmlift2lem12  31603  neibastop2lem  32661  onint1  32754  icoreunrn  33518  cnfin0  33551  opnmbllem0  33758  heibor1  33922  unichnidl  34143  prtlem16  34658  prter2  34670  truniALT  39253  unipwrVD  39566  unipwr  39567  truniALTVD  39613  unisnALT  39661  restuni3  39800  disjinfi  39879  stoweidlem43  40763  stoweidlem55  40775  salexct  41055
 Copyright terms: Public domain W3C validator