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 2828	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵))
2		eleq1 2827	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	anbi12d 638	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶)))
4	3	spcegv 3535	. . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)))
5	4	anabsi7 677	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
6		eluni 4841	. 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
7	5, 6	sylibr 235	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547  ∃wex 1786   ∈ wcel 2119  ∪ cuni 4838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-uni 4839

This theorem is referenced by:  ssuni  4863  unipw  5389  opeluu  5410  unon  7771  limuni3  7792  naddsuc2  8627  uniinqs  8734  trcl  9640  rankwflemb  9708  ac5num  9949  dfac3  10034  isf34lem4  10290  axcclem  10370  ttukeylem7  10428  brdom7disj  10444  brdom6disj  10445  wrdexb  14478  dprdfeq0  19990  tgss2  22970  ppttop  22990  isclo  23070  neips  23096  2ndcomap  23441  2ndcsep  23442  locfincmp  23509  comppfsc  23515  txkgen  23635  txconn  23672  basqtop  23694  nrmr0reg  23732  alexsublem  24027  alexsubALTlem4  24033  alexsubALT  24034  ptcmplem4  24038  unirnblps  24402  unirnbl  24403  blbas  24413  met2ndci  24505  bndth  24943  dyadmbllem  25584  opnmbllem  25586  ssdifidllem  33539  ssmxidllem  33556  dya2iocnei  34466  dstfrvunirn  34659  pconnconn  35459  cvmcov2  35503  cvmlift2lem11  35541  cvmlift2lem12  35542  neibastop2lem  36588  onint1  36677  ttcid  36720  ttctr  36721  dfttc2g  36734  icoreunrn  37721  opnmbllem0  38023  heibor1  38177  unichnidl  38398  prtlem16  39361  prter2  39373  truniALT  44985  unipwrVD  45275  unipwr  45276  truniALTVD  45321  unisnALT  45369  permaxun  45455  restuni3  45565  disjinfi  45639  stoweidlem43  46486  stoweidlem55  46498  salexct  46777