Theorem elin2 4104

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

Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ∩ cin 3859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3867

This theorem is referenced by:  elin3  4107  opelres  5834  elpredim  6143  elpred  6144  elpredg  6145  fnres  6462  funfvima  6990  fnwelem  7836  ressuppssdif  7865  fz1isolem  13884  isabl  18990  isfld  19592  2idlcpbl  20088  qus1  20089  qusrhm  20091  isidom  20158  lmres  22013  isnvc  23410  cvslvec  23839  cvsclm  23840  iscvs  23841  cvsi  23844  ishl  24075  ply1pid  24892  rplogsum  26223  iscusgr  27320  isphg  28712  ishlo  28782  hhsscms  29173  mayete3i  29623  isogrp  30866  isofld  31039  sltres  33462  bj-elid6  34899  bj-isrvec  35022  caures  35512  iscrngo  35748  fldcrng  35756  isdmn  35806  isolat  36822  srhmsubclem1  45113  srhmsubc  45116  srhmsubcALTV  45134