Theorem elin2 4156

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 2855	. 2 ⊢ (𝐴 ∈ 𝑋 ↔ 𝐴 ∈ (𝐵 ∩ 𝐶))
3		elin 3921	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
4	2, 3	bitri 278	1 ⊢ (𝐴 ∈ 𝑋 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143   ∩ cin 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912

This theorem is referenced by:  elin3  4159  opelres  5984  elpredgg  6315  fnres  6662  funfvima  7228  fnwelem  8123  ressuppssdif  8177  fz1isolem  14494  isabl  19849  isogrp  20189  srhmsubclem1  20776  srhmsubc  20779  isidom  20823  isfld  20840  isofld  20967  2idlelb  21392  qus1  21413  qusrhm  21415  lmres  23457  isnvc  24852  cvslvec  25284  cvsclm  25285  iscvs  25286  cvsi  25289  ishl  25521  ply1pid  26340  rplogsum  27691  ltsres  27826  iscusgr  29768  isphg  31169  ishlo  31239  hhsscms  31630  mayete3i  32080  bj-elid6  37814  bj-isrvec  37938  caures  38411  iscrngo  38647  fldcrngo  38655  isdmn  38705  isolat  39986  srhmsubcALTV  49090  isidom2  49109