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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-uni 4868

This theorem is referenced by:  ssuni  4892  unipw  5405  opeluu  5425  unon  7786  limuni3  7808  naddsuc2  8642  uniinqs  8747  trcl  9657  rankwflemb  9722  ac5num  9965  dfac3  10050  isf34lem4  10306  axcclem  10386  ttukeylem7  10444  brdom7disj  10460  brdom6disj  10461  wrdexb  14466  dprdfeq0  19938  tgss2  22907  ppttop  22927  isclo  23007  neips  23033  2ndcomap  23378  2ndcsep  23379  locfincmp  23446  comppfsc  23452  txkgen  23572  txconn  23609  basqtop  23631  nrmr0reg  23669  alexsublem  23964  alexsubALTlem4  23970  alexsubALT  23971  ptcmplem4  23975  unirnblps  24340  unirnbl  24341  blbas  24351  met2ndci  24443  bndth  24890  dyadmbllem  25533  opnmbllem  25535  ssdifidllem  33420  ssmxidllem  33437  dya2iocnei  34266  dstfrvunirn  34459  pconnconn  35211  cvmcov2  35255  cvmlift2lem11  35293  cvmlift2lem12  35294  neibastop2lem  36341  onint1  36430  icoreunrn  37340  opnmbllem0  37643  heibor1  37797  unichnidl  38018  prtlem16  38855  prter2  38867  truniALT  44524  unipwrVD  44814  unipwr  44815  truniALTVD  44860  unisnALT  44908  permaxun  44994  restuni3  45105  disjinfi  45179  stoweidlem43  46034  stoweidlem55  46046  salexct  46325