Theorem elin2 4166

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ∩ cin 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-in 3921

This theorem is referenced by:  elin3  4169  opelres  5956  elpredgg  6287  fnres  6645  funfvima  7204  fnwelem  8110  ressuppssdif  8164  fz1isolem  14426  isabl  19714  srhmsubclem1  20586  srhmsubc  20589  isidom  20634  isfld  20649  2idlelb  21163  qus1  21184  qusrhm  21186  lmres  23187  isnvc  24583  cvslvec  25025  cvsclm  25026  iscvs  25027  cvsi  25030  ishl  25262  ply1pid  26088  rplogsum  27438  sltres  27574  iscusgr  29345  isphg  30746  ishlo  30816  hhsscms  31207  mayete3i  31657  isogrp  33016  isofld  33280  bj-elid6  37158  bj-isrvec  37282  caures  37754  iscrngo  37990  fldcrngo  37998  isdmn  38048  isolat  39205  srhmsubcALTV  48313