Theorem elunii 4856

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-uni 4852

This theorem is referenced by:  ssuni  4876  unipw  5398  opeluu  5419  unon  7776  limuni3  7797  naddsuc2  8631  uniinqs  8738  trcl  9643  rankwflemb  9711  ac5num  9952  dfac3  10037  isf34lem4  10293  axcclem  10373  ttukeylem7  10431  brdom7disj  10447  brdom6disj  10448  wrdexb  14481  dprdfeq0  19993  tgss2  22965  ppttop  22985  isclo  23065  neips  23091  2ndcomap  23436  2ndcsep  23437  locfincmp  23504  comppfsc  23510  txkgen  23630  txconn  23667  basqtop  23689  nrmr0reg  23727  alexsublem  24022  alexsubALTlem4  24028  alexsubALT  24029  ptcmplem4  24033  unirnblps  24397  unirnbl  24398  blbas  24408  met2ndci  24500  bndth  24938  dyadmbllem  25579  opnmbllem  25581  ssdifidllem  33534  ssmxidllem  33551  dya2iocnei  34445  dstfrvunirn  34638  pconnconn  35432  cvmcov2  35476  cvmlift2lem11  35514  cvmlift2lem12  35515  neibastop2lem  36561  onint1  36650  ttcid  36693  ttctr  36694  dfttc2g  36707  icoreunrn  37692  opnmbllem0  37994  heibor1  38148  unichnidl  38369  prtlem16  39332  prter2  39344  truniALT  44989  unipwrVD  45279  unipwr  45280  truniALTVD  45325  unisnALT  45373  permaxun  45459  restuni3  45569  disjinfi  45643  stoweidlem43  46492  stoweidlem55  46504  salexct  46783