Theorem elunii 4872

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∪ cuni 4867

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-uni 4868

This theorem is used by:  ssuni  4893  unipw  5418  opeluu  5439  unon  7840  limuni3  7861  naddsuc2  8704  uniinqs  8811  trcl  9722  rankwflemb  9793  rankwflembOLD  9794  ac5num  10108  dfac3  10193  isf34lem4  10448  axcclem  10528  ttukeylem7  10586  brdom7disj  10603  brdom6disj  10604  wrdexb  14663  dprdfeq0  20231  unichnlidl  21509  ssdifidllem  21633  tgss2  23298  ppttop  23318  isclo  23398  neips  23424  2ndcomap  23770  2ndcsep  23771  locfincmp  23838  comppfsc  23844  txkgen  23964  txconn  24001  basqtop  24023  nrmr0reg  24061  alexsublem  24356  alexsubALTlem4  24362  alexsubALT  24363  ptcmplem4  24367  unirnblps  24731  unirnbl  24732  blbas  24742  met2ndci  24834  bndth  25272  dyadmbllem  25913  opnmbllem  25915  ssmxidllem  33991  dya2iocnei  34907  dstfrvunirn  35100  pconnconn  35975  cvmcov2  36019  cvmlift2lem11  36057  cvmlift2lem12  36058  neibastop2lem  37128  onint1  37217  ttcid  37260  ttctr  37261  dfttc2g  37274  icoreunrn  38262  opnmbllem0  38554  heibor1  38724  unichnidl  38945  prtlem16  39906  prter2  39918  truniALT  45509  unipwrVD  45799  unipwr  45800  truniALTVD  45845  unisnALT  45893  permaxun  45979  restuni3  46102  disjinfi  46176  stoweidlem43  47022  stoweidlem55  47034  salexct  47313