Theorem elin2 4154

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

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

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 3438  df-in 3910

This theorem is referenced by:  elin3  4157  opelres  5936  elpredgg  6262  fnres  6609  funfvima  7166  fnwelem  8064  ressuppssdif  8118  fz1isolem  14368  isabl  19663  isogrp  20003  srhmsubclem1  20562  srhmsubc  20565  isidom  20610  isfld  20625  isofld  20749  2idlelb  21160  qus1  21181  qusrhm  21183  lmres  23185  isnvc  24581  cvslvec  25023  cvsclm  25024  iscvs  25025  cvsi  25028  ishl  25260  ply1pid  26086  rplogsum  27436  sltres  27572  iscusgr  29363  isphg  30761  ishlo  30831  hhsscms  31222  mayete3i  31672  bj-elid6  37148  bj-isrvec  37272  caures  37744  iscrngo  37980  fldcrngo  37988  isdmn  38038  isolat  39195  srhmsubcALTV  48313