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

Theorem elunii 4432
 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 2688 . . . . 5 (𝑥 = 𝐵 → (𝐴𝑥𝐴𝐵))
2 eleq1 2687 . . . . 5 (𝑥 = 𝐵 → (𝑥𝐶𝐵𝐶))
31, 2anbi12d 746 . . . 4 (𝑥 = 𝐵 → ((𝐴𝑥𝑥𝐶) ↔ (𝐴𝐵𝐵𝐶)))
43spcegv 3289 . . 3 (𝐵𝐶 → ((𝐴𝐵𝐵𝐶) → ∃𝑥(𝐴𝑥𝑥𝐶)))
54anabsi7 859 . 2 ((𝐴𝐵𝐵𝐶) → ∃𝑥(𝐴𝑥𝑥𝐶))
6 eluni 4430 . 2 (𝐴 𝐶 ↔ ∃𝑥(𝐴𝑥𝑥𝐶))
75, 6sylibr 224 1 ((𝐴𝐵𝐵𝐶) → 𝐴 𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   = wceq 1481  ∃wex 1702   ∈ wcel 1988  ∪ cuni 4427 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-uni 4428 This theorem is referenced by:  ssuni  4450  ssuniOLD  4451  unipw  4909  opeluu  4930  unon  7016  limuni3  7037  uniinqs  7812  trcl  8589  rankwflemb  8641  ac5num  8844  dfac3  8929  isf34lem4  9184  axcclem  9264  ttukeylem7  9322  brdom7disj  9338  brdom6disj  9339  wrdexb  13299  dprdfeq0  18402  tgss2  20772  ppttop  20792  isclo  20872  neips  20898  2ndcomap  21242  2ndcsep  21243  locfincmp  21310  comppfsc  21316  txkgen  21436  txconn  21473  basqtop  21495  nrmr0reg  21533  alexsublem  21829  alexsubALTlem4  21835  alexsubALT  21836  ptcmplem4  21840  unirnblps  22205  unirnbl  22206  blbas  22216  met2ndci  22308  bndth  22738  dyadmbllem  23348  opnmbllem  23350  dya2iocnei  30318  dstfrvunirn  30510  pconnconn  31187  cvmcov2  31231  cvmlift2lem11  31269  cvmlift2lem12  31270  neibastop2lem  32330  onint1  32423  icoreunrn  33178  opnmbllem0  33416  heibor1  33580  unichnidl  33801  prtlem16  33973  prter2  33985  truniALT  38571  unipwrVD  38887  unipwr  38888  truniALTVD  38934  unisnALT  38982  restuni3  39121  disjinfi  39196  stoweidlem43  40023  stoweidlem55  40035  salexct  40315
 Copyright terms: Public domain W3C validator