Theorem elin2 4176

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

Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114   ∩ cin 3937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945

This theorem is referenced by:  elin3  4179  opelres  5861  elpredim  6162  elpred  6163  elpredg  6164  fnres  6476  funfvima  6994  fnwelem  7827  ressuppssdif  7853  fz1isolem  13822  isabl  18912  isfld  19513  2idlcpbl  20009  qus1  20010  qusrhm  20012  isidom  20079  lmres  21910  isnvc  23306  cvslvec  23731  cvsclm  23732  iscvs  23733  cvsi  23736  ishl  23967  ply1pid  24775  rplogsum  26105  iscusgr  27202  isphg  28596  ishlo  28666  hhsscms  29057  mayete3i  29507  isogrp  30705  isofld  30877  sltres  33171  bj-elid6  34464  bj-isrvec  34577  caures  35037  iscrngo  35276  fldcrng  35284  isdmn  35334  isolat  36350  srhmsubclem1  44351  srhmsubc  44354  srhmsubcALTV  44372