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  7827  limuni3  7848  naddsuc2  8690  uniinqs  8797  trcl  9707  rankwflemb  9775  ac5num  10039  dfac3  10124  isf34lem4  10379  axcclem  10459  ttukeylem7  10517  brdom7disj  10534  brdom6disj  10535  wrdexb  14590  dprdfeq0  20151  unichnlidl  21425  ssdifidllem  21547  tgss2  23212  ppttop  23232  isclo  23312  neips  23338  2ndcomap  23684  2ndcsep  23685  locfincmp  23752  comppfsc  23758  txkgen  23878  txconn  23915  basqtop  23937  nrmr0reg  23975  alexsublem  24270  alexsubALTlem4  24276  alexsubALT  24277  ptcmplem4  24281  unirnblps  24645  unirnbl  24646  blbas  24656  met2ndci  24748  bndth  25186  dyadmbllem  25827  opnmbllem  25829  ssmxidllem  33876  dya2iocnei  34793  dstfrvunirn  34986  pconnconn  35810  cvmcov2  35854  cvmlift2lem11  35892  cvmlift2lem12  35893  neibastop2lem  36979  onint1  37068  ttcid  37111  ttctr  37112  dfttc2g  37125  icoreunrn  38113  opnmbllem0  38405  heibor1  38560  unichnidl  38781  prtlem16  39742  prter2  39754  truniALT  45364  unipwrVD  45654  unipwr  45655  truniALTVD  45700  unisnALT  45748  permaxun  45834  restuni3  45950  disjinfi  46024  stoweidlem43  46871  stoweidlem55  46883  salexct  47162