Theorem elunii 4855

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 2825	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵))
2		eleq1 2824	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	anbi12d 633	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶)))
4	3	spcegv 3539	. . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)))
5	4	anabsi7 672	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
6		eluni 4853	. 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
7	5, 6	sylibr 234	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∪ cuni 4850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-uni 4851

This theorem is referenced by:  ssuni  4875  unipw  5402  opeluu  5423  unon  7782  limuni3  7803  naddsuc2  8637  uniinqs  8744  trcl  9649  rankwflemb  9717  ac5num  9958  dfac3  10043  isf34lem4  10299  axcclem  10379  ttukeylem7  10437  brdom7disj  10453  brdom6disj  10454  wrdexb  14487  dprdfeq0  19999  tgss2  22952  ppttop  22972  isclo  23052  neips  23078  2ndcomap  23423  2ndcsep  23424  locfincmp  23491  comppfsc  23497  txkgen  23617  txconn  23654  basqtop  23676  nrmr0reg  23714  alexsublem  24009  alexsubALTlem4  24015  alexsubALT  24016  ptcmplem4  24020  unirnblps  24384  unirnbl  24385  blbas  24395  met2ndci  24487  bndth  24925  dyadmbllem  25566  opnmbllem  25568  ssdifidllem  33516  ssmxidllem  33533  dya2iocnei  34426  dstfrvunirn  34619  pconnconn  35413  cvmcov2  35457  cvmlift2lem11  35495  cvmlift2lem12  35496  neibastop2lem  36542  onint1  36631  ttcid  36674  ttctr  36675  dfttc2g  36688  icoreunrn  37675  opnmbllem0  37977  heibor1  38131  unichnidl  38352  prtlem16  39315  prter2  39327  truniALT  44968  unipwrVD  45258  unipwr  45259  truniALTVD  45304  unisnALT  45352  permaxun  45438  restuni3  45548  disjinfi  45622  stoweidlem43  46471  stoweidlem55  46483  salexct  46762