Theorem elunii 4881

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 2858	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵))
2		eleq1 2857	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	anbi12d 643	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶)))
4	3	spcegv 3565	. . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)))
5	4	anabsi7 683	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
6		eluni 4879	. 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
7	5, 6	sylibr 237	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567  ∃wex 1806   ∈ wcel 2149  ∪ cuni 4876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-uni 4877

This theorem is referenced by:  ssuni  4902  unipw  5432  opeluu  5453  unon  7826  limuni3  7847  naddsuc2  8687  uniinqs  8794  trcl  9696  rankwflemb  9764  ac5num  10019  dfac3  10104  isf34lem4  10360  axcclem  10440  ttukeylem7  10498  brdom7disj  10514  brdom6disj  10515  wrdexb  14561  dprdfeq0  20093  unichnlidl  21339  ssdifidllem  21452  tgss2  23112  ppttop  23132  isclo  23212  neips  23238  2ndcomap  23583  2ndcsep  23584  locfincmp  23651  comppfsc  23657  txkgen  23777  txconn  23814  basqtop  23836  nrmr0reg  23874  alexsublem  24169  alexsubALTlem4  24175  alexsubALT  24176  ptcmplem4  24180  unirnblps  24544  unirnbl  24545  blbas  24555  met2ndci  24647  bndth  25085  dyadmbllem  25726  opnmbllem  25728  ssmxidllem  33700  dya2iocnei  34616  dstfrvunirn  34809  pconnconn  35621  cvmcov2  35665  cvmlift2lem11  35703  cvmlift2lem12  35704  neibastop2lem  36759  onint1  36848  ttcid  36891  ttctr  36892  dfttc2g  36905  icoreunrn  37892  opnmbllem0  38194  heibor1  38348  unichnidl  38569  prtlem16  39532  prter2  39544  truniALT  45141  unipwrVD  45431  unipwr  45432  truniALTVD  45477  unisnALT  45525  permaxun  45611  restuni3  45727  disjinfi  45801  stoweidlem43  46648  stoweidlem55  46660  salexct  46939