Theorem elunii 4879

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 2818	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵))
2		eleq1 2817	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	anbi12d 632	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶)))
4	3	spcegv 3566	. . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)))
5	4	anabsi7 671	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
6		eluni 4877	. 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
7	5, 6	sylibr 234	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∪ cuni 4874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-uni 4875

This theorem is referenced by:  ssuni  4899  unipw  5413  opeluu  5433  unon  7809  limuni3  7831  naddsuc2  8668  uniinqs  8773  trcl  9688  rankwflemb  9753  ac5num  9996  dfac3  10081  isf34lem4  10337  axcclem  10417  ttukeylem7  10475  brdom7disj  10491  brdom6disj  10492  wrdexb  14497  dprdfeq0  19961  tgss2  22881  ppttop  22901  isclo  22981  neips  23007  2ndcomap  23352  2ndcsep  23353  locfincmp  23420  comppfsc  23426  txkgen  23546  txconn  23583  basqtop  23605  nrmr0reg  23643  alexsublem  23938  alexsubALTlem4  23944  alexsubALT  23945  ptcmplem4  23949  unirnblps  24314  unirnbl  24315  blbas  24325  met2ndci  24417  bndth  24864  dyadmbllem  25507  opnmbllem  25509  ssdifidllem  33434  ssmxidllem  33451  dya2iocnei  34280  dstfrvunirn  34473  pconnconn  35225  cvmcov2  35269  cvmlift2lem11  35307  cvmlift2lem12  35308  neibastop2lem  36355  onint1  36444  icoreunrn  37354  opnmbllem0  37657  heibor1  37811  unichnidl  38032  prtlem16  38869  prter2  38881  truniALT  44538  unipwrVD  44828  unipwr  44829  truniALTVD  44874  unisnALT  44922  permaxun  45008  restuni3  45119  disjinfi  45193  stoweidlem43  46048  stoweidlem55  46060  salexct  46339