Theorem elunii 4845

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 2828	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵))
2		eleq1 2827	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	anbi12d 631	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶)))
4	3	spcegv 3537	. . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)))
5	4	anabsi7 668	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
6		eluni 4843	. 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
7	5, 6	sylibr 233	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539  ∃wex 1782   ∈ wcel 2107  ∪ cuni 4840

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-uni 4841

This theorem is referenced by:  ssuni  4867  unipw  5367  opeluu  5386  unon  7687  limuni3  7708  uniinqs  8595  trcl  9495  rankwflemb  9560  ac5num  9801  dfac3  9886  isf34lem4  10142  axcclem  10222  ttukeylem7  10280  brdom7disj  10296  brdom6disj  10297  wrdexb  14237  dprdfeq0  19634  tgss2  22146  ppttop  22166  isclo  22247  neips  22273  2ndcomap  22618  2ndcsep  22619  locfincmp  22686  comppfsc  22692  txkgen  22812  txconn  22849  basqtop  22871  nrmr0reg  22909  alexsublem  23204  alexsubALTlem4  23210  alexsubALT  23211  ptcmplem4  23215  unirnblps  23581  unirnbl  23582  blbas  23592  met2ndci  23687  bndth  24130  dyadmbllem  24772  opnmbllem  24774  ssmxidllem  31650  dya2iocnei  32258  dstfrvunirn  32450  pconnconn  33202  cvmcov2  33246  cvmlift2lem11  33284  cvmlift2lem12  33285  neibastop2lem  34558  onint1  34647  icoreunrn  35539  opnmbllem0  35822  heibor1  35977  unichnidl  36198  prtlem16  36890  prter2  36902  truniALT  42168  unipwrVD  42459  unipwr  42460  truniALTVD  42505  unisnALT  42553  restuni3  42674  disjinfi  42738  stoweidlem43  43591  stoweidlem55  43603  salexct  43880