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.

Step	Hyp	Ref	Expression
1		eleq2 2677	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵))
2		eleq1 2676	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	anbi12d 743	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶)))
4	3	spcegv 3267	. . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)))
5	4	anabsi7 856	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
6		eluni 4375	. 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
7	5, 6	sylibr 223	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)

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