Theorem elunii 4872

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.

Step	Hyp	Ref	Expression
1		eleq2 2849	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵))
2		eleq1 2848	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	anbi12d 644	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶)))
4	3	spcegv 3551	. . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)))
5	4	anabsi7 684	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
6		eluni 4870	. 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
7	5, 6	sylibr 237	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∪ cuni 4867

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-uni 4868

This theorem is used by:  ssuni  4893  unipw  5425  opeluu  5446  unon  7828  limuni3  7849  naddsuc2  8693  uniinqs  8800  trcl  9710  rankwflemb  9778  ac5num  10042  dfac3  10127  isf34lem4  10382  axcclem  10462  ttukeylem7  10520  brdom7disj  10537  brdom6disj  10538  wrdexb  14593  dprdfeq0  20154  unichnlidl  21428  ssdifidllem  21550  tgss2  23215  ppttop  23235  isclo  23315  neips  23341  2ndcomap  23687  2ndcsep  23688  locfincmp  23755  comppfsc  23761  txkgen  23881  txconn  23918  basqtop  23940  nrmr0reg  23978  alexsublem  24273  alexsubALTlem4  24279  alexsubALT  24280  ptcmplem4  24284  unirnblps  24648  unirnbl  24649  blbas  24659  met2ndci  24751  bndth  25189  dyadmbllem  25830  opnmbllem  25832  ssmxidllem  33879  dya2iocnei  34796  dstfrvunirn  34989  pconnconn  35813  cvmcov2  35857  cvmlift2lem11  35895  cvmlift2lem12  35896  neibastop2lem  36982  onint1  37071  ttcid  37114  ttctr  37115  dfttc2g  37128  icoreunrn  38116  opnmbllem0  38408  heibor1  38563  unichnidl  38784  prtlem16  39745  prter2  39757  truniALT  45367  unipwrVD  45657  unipwr  45658  truniALTVD  45703  unisnALT  45751  permaxun  45837  restuni3  45953  disjinfi  46027  stoweidlem43  46874  stoweidlem55  46886  salexct  47165