Theorem elin2 4000

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

Syntax hints:   ↔ wb 197   ∧ wa 384   = wceq 1637   ∈ wcel 2156   ∩ cin 3768

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-in 3776

This theorem is referenced by:  elin3  4003  elpredim  5905  elpred  5906  elpredg  5907  fnres  6214  funfvima  6713  fnwelem  7522  ressuppssdif  7546  fz1isolem  13458  isabl  18394  isfld  18956  2idlcpbl  19439  qus1  19440  qusrhm  19442  isidom  19509  lmres  21315  isnvc  22709  cvslvec  23134  cvsclm  23135  iscvs  23136  ishl  23368  ply1pid  24152  rplogsum  25429  iscusgr  26541  isphg  27999  ishlo  28070  hhsscms  28463  mayete3i  28914  isogrp  30026  isofld  30126  sltres  32134  caures  33865  iscrngo  34104  fldcrng  34112  isdmn  34162  opelresALTV  34347  isolat  34990  srhmsubclem1  42638  srhmsubc  42641  srhmsubcALTV  42659