Theorem elin2 4173

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

Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1533   ∈ wcel 2110   ∩ cin 3934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3942

This theorem is referenced by:  elin3  4176  opelres  5853  elpredim  6154  elpred  6155  elpredg  6156  fnres  6468  funfvima  6986  fnwelem  7819  ressuppssdif  7845  fz1isolem  13813  isabl  18904  isfld  19505  2idlcpbl  20001  qus1  20002  qusrhm  20004  isidom  20071  lmres  21902  isnvc  23298  cvslvec  23723  cvsclm  23724  iscvs  23725  cvsi  23728  ishl  23959  ply1pid  24767  rplogsum  26097  iscusgr  27194  isphg  28588  ishlo  28658  hhsscms  29049  mayete3i  29499  isogrp  30698  isofld  30870  sltres  33164  bj-elid6  34456  bj-isrvec  34569  caures  35029  iscrngo  35268  fldcrng  35276  isdmn  35326  isolat  36342  srhmsubclem1  44338  srhmsubc  44341  srhmsubcALTV  44359