Theorem elin2 4127

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

Syntax hints:   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890

This theorem is referenced by:  elin3  4130  opelres  5886  elpredgg  6204  fnres  6543  funfvima  7088  fnwelem  7943  ressuppssdif  7972  fz1isolem  14103  isabl  19305  isfld  19915  2idlcpbl  20418  qus1  20419  qusrhm  20421  isidom  20488  lmres  22359  isnvc  23765  cvslvec  24194  cvsclm  24195  iscvs  24196  cvsi  24199  ishl  24431  ply1pid  25249  rplogsum  26580  iscusgr  27688  isphg  29080  ishlo  29150  hhsscms  29541  mayete3i  29991  isogrp  31230  isofld  31403  sltres  33792  bj-elid6  35268  bj-isrvec  35392  caures  35845  iscrngo  36081  fldcrng  36089  isdmn  36139  isolat  37153  srhmsubclem1  45519  srhmsubc  45522  srhmsubcALTV  45540