Theorem elunii 4843

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 2901	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵))
2		eleq1 2900	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	anbi12d 632	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶)))
4	3	spcegv 3597	. . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)))
5	4	anabsi7 669	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
6		eluni 4841	. 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
7	5, 6	sylibr 236	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537  ∃wex 1780   ∈ wcel 2114  ∪ cuni 4838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-uni 4839

This theorem is referenced by:  ssuni  4863  unipw  5343  opeluu  5362  unon  7546  limuni3  7567  uniinqs  8377  trcl  9170  rankwflemb  9222  ac5num  9462  dfac3  9547  isf34lem4  9799  axcclem  9879  ttukeylem7  9937  brdom7disj  9953  brdom6disj  9954  wrdexb  13874  dprdfeq0  19144  tgss2  21595  ppttop  21615  isclo  21695  neips  21721  2ndcomap  22066  2ndcsep  22067  locfincmp  22134  comppfsc  22140  txkgen  22260  txconn  22297  basqtop  22319  nrmr0reg  22357  alexsublem  22652  alexsubALTlem4  22658  alexsubALT  22659  ptcmplem4  22663  unirnblps  23029  unirnbl  23030  blbas  23040  met2ndci  23132  bndth  23562  dyadmbllem  24200  opnmbllem  24202  ssmxidllem  30978  dya2iocnei  31540  dstfrvunirn  31732  pconnconn  32478  cvmcov2  32522  cvmlift2lem11  32560  cvmlift2lem12  32561  neibastop2lem  33708  onint1  33797  icoreunrn  34643  opnmbllem0  34943  heibor1  35103  unichnidl  35324  prtlem16  36020  prter2  36032  truniALT  40895  unipwrVD  41186  unipwr  41187  truniALTVD  41232  unisnALT  41280  restuni3  41404  disjinfi  41474  stoweidlem43  42348  stoweidlem55  42360  salexct  42637