Theorem elunii 4871

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 2849	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵))
2		eleq1 2848	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	anbi12d 644	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶)))
4	3	spcegv 3551	. . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)))
5	4	anabsi7 684	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
6		eluni 4869	. 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
7	5, 6	sylibr 237	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569  ∃wex 1811   ∈ wcel 2144  ∪ cuni 4866

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-uni 4867

This theorem is used by:  ssuni  4892  unipw  5418  opeluu  5439  unon  7846  limuni3  7867  naddsuc2  8718  uniinqs  8825  trcl  9736  rankwflemb  9807  rankwflembOLD  9808  ac5num  10122  dfac3  10207  isf34lem4  10462  axcclem  10542  ttukeylem7  10600  brdom7disj  10617  brdom6disj  10618  wrdexb  14677  dprdfeq0  20247  unichnlidl  21525  ssdifidllem  21649  tgss2  23314  ppttop  23334  isclo  23414  neips  23440  2ndcomap  23786  2ndcsep  23787  locfincmp  23854  comppfsc  23860  txkgen  23980  txconn  24017  basqtop  24039  nrmr0reg  24077  alexsublem  24372  alexsubALTlem4  24378  alexsubALT  24379  ptcmplem4  24383  unirnblps  24747  unirnbl  24748  blbas  24758  met2ndci  24850  bndth  25288  dyadmbllem  25929  opnmbllem  25931  ssmxidllem  34048  dya2iocnei  34964  dstfrvunirn  35157  pconnconn  36086  cvmcov2  36130  cvmlift2lem11  36168  cvmlift2lem12  36169  neibastop2lem  37244  onint1  37333  ttcid  37376  ttctr  37377  dfttc2g  37390  icoreunrn  38391  opnmbllem0  38683  heibor1  38853  unichnidl  39074  prtlem16  40035  prter2  40047  truniALT  45632  unipwrVD  45922  unipwr  45923  truniALTVD  45968  unisnALT  46016  permaxun  46109  restuni3  46241  disjinfi  46315  stoweidlem43  47161  stoweidlem55  47173  salexct  47452