Theorem elin2 4149

Description: Membership in a class defined as an intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.)

Hypothesis

Ref	Expression
elin2.x	⊢ 𝑋 = (𝐵 ∩ 𝐶)

Assertion

Ref	Expression
elin2	⊢ (𝐴 ∈ 𝑋 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Proof of Theorem elin2

Step	Hyp	Ref	Expression
1		elin2.x	. . 3 ⊢ 𝑋 = (𝐵 ∩ 𝐶)
2	1	eleq2i 2853	. 2 ⊢ (𝐴 ∈ 𝑋 ↔ 𝐴 ∈ (𝐵 ∩ 𝐶))
3		elin 3915	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
4	2, 3	bitri 278	1 ⊢ (𝐴 ∈ 𝑋 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ∩ cin 3898

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-in 3906

This theorem is used by:  elin3  4152  opelres  5976  elpredgg  6317  fnres  6666  funfvima  7236  fnwelem  8143  ressuppssdif  8202  fz1isolem  14606  isabl  19998  isogrp  20338  srhmsubclem1  20929  srhmsubc  20932  isidom  20976  isfld  20993  isofld  21121  2idlelb  21546  qus1  21568  qusrhm  21570  lmres  23618  isnvc  25014  cvslvec  25446  cvsclm  25447  iscvs  25448  cvsi  25451  ishl  25683  ply1pid  26501  rplogsum  27854  ltsres  28019  iscusgr  29999  isphg  31419  ishlo  31489  hhsscms  31880  mayete3i  32330  bj-elid6  38091  bj-isrvec  38215  caures  38694  iscrngo  38930  fldcrngo  38938  isdmn  38988  isolat  40269  srhmsubcALTV  49421  isidom2  49440