Theorem elunii 4752

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 2870	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵))
2		eleq1 2869	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	anbi12d 630	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶)))
4	3	spcegv 3538	. . 3 ⊢ (𝐵 ∈ 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶)))
5	4	anabsi7 667	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
6		eluni 4750	. 2 ⊢ (𝐴 ∈ ∪ 𝐶 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶))
7	5, 6	sylibr 235	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1522  ∃wex 1762   ∈ wcel 2080  ∪ cuni 4747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-ext 2768

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-v 3438  df-uni 4748

This theorem is referenced by:  ssuni  4769  unipw  5237  opeluu  5257  unon  7405  limuni3  7426  uniinqs  8230  trcl  9019  rankwflemb  9071  ac5num  9311  dfac3  9396  isf34lem4  9648  axcclem  9728  ttukeylem7  9786  brdom7disj  9802  brdom6disj  9803  wrdexb  13719  dprdfeq0  18861  tgss2  21279  ppttop  21299  isclo  21379  neips  21405  2ndcomap  21750  2ndcsep  21751  locfincmp  21818  comppfsc  21824  txkgen  21944  txconn  21981  basqtop  22003  nrmr0reg  22041  alexsublem  22336  alexsubALTlem4  22342  alexsubALT  22343  ptcmplem4  22347  unirnblps  22712  unirnbl  22713  blbas  22723  met2ndci  22815  bndth  23245  dyadmbllem  23883  opnmbllem  23885  dya2iocnei  31149  dstfrvunirn  31341  pconnconn  32080  cvmcov2  32124  cvmlift2lem11  32162  cvmlift2lem12  32163  neibastop2lem  33311  onint1  33400  icoreunrn  34184  opnmbllem0  34472  heibor1  34633  unichnidl  34854  prtlem16  35549  prter2  35561  truniALT  40427  unipwrVD  40718  unipwr  40719  truniALTVD  40764  unisnALT  40812  restuni3  40937  disjinfi  41007  stoweidlem43  41884  stoweidlem55  41896  salexct  42173