Theorem elin2 4099

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144   ∩ cin 4088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 4090

This theorem is used by:  elin3  4102  opelres  5977  elpredgg  6320  fnres  6671  funfvima  7240  fnwelem  8150  ressuppssdif  8210  fz1isolem  14613  isabl  20007  isogrp  20347  srhmsubclem1  20938  srhmsubc  20941  isidom  20985  isfld  21002  isofld  21130  2idlelb  21555  qus1  21577  qusrhm  21579  lmres  23627  isnvc  25023  cvslvec  25455  cvsclm  25456  iscvs  25457  cvsi  25460  ishl  25692  ply1pid  26510  rplogsum  27863  ltsres  28028  iscusgr  30008  isphg  31428  ishlo  31498  hhsscms  31889  mayete3i  32339  fwfffunres  35768  bj-elid6  38228  bj-isrvec  38352  caures  38831  iscrngo  39067  fldcrngo  39075  isdmn  39125  isolat  40406  srhmsubcALTV  49558  isidom2  49577