Theorem elin2 4150

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2111   ∩ cin 3896

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3904

This theorem is referenced by:  elin3  4153  opelres  5933  elpredgg  6261  fnres  6608  funfvima  7164  fnwelem  8061  ressuppssdif  8115  fz1isolem  14368  isabl  19696  isogrp  20036  srhmsubclem1  20592  srhmsubc  20595  isidom  20640  isfld  20655  isofld  20779  2idlelb  21190  qus1  21211  qusrhm  21213  lmres  23215  isnvc  24610  cvslvec  25052  cvsclm  25053  iscvs  25054  cvsi  25057  ishl  25289  ply1pid  26115  rplogsum  27465  sltres  27601  iscusgr  29396  isphg  30797  ishlo  30867  hhsscms  31258  mayete3i  31708  bj-elid6  37214  bj-isrvec  37338  caures  37810  iscrngo  38046  fldcrngo  38054  isdmn  38104  isolat  39321  srhmsubcALTV  48435