Theorem elin2 4178

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-in 3933

This theorem is referenced by:  elin3  4181  opelres  5972  elpredgg  6303  fnres  6665  funfvima  7222  fnwelem  8130  ressuppssdif  8184  fz1isolem  14479  isabl  19765  srhmsubclem1  20637  srhmsubc  20640  isidom  20685  isfld  20700  2idlelb  21214  qus1  21235  qusrhm  21237  lmres  23238  isnvc  24634  cvslvec  25076  cvsclm  25077  iscvs  25078  cvsi  25081  ishl  25314  ply1pid  26140  rplogsum  27490  sltres  27626  iscusgr  29397  isphg  30798  ishlo  30868  hhsscms  31259  mayete3i  31709  isogrp  33070  isofld  33324  bj-elid6  37188  bj-isrvec  37312  caures  37784  iscrngo  38020  fldcrngo  38028  isdmn  38078  isolat  39230  srhmsubcALTV  48300