Theorem elin2 4149

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3906

This theorem is used by:  elin3  4152  opelres  5978  elpredgg  6312  fnres  6660  funfvima  7230  fnwelem  8130  ressuppssdif  8184  fz1isolem  14527  isabl  19912  isogrp  20252  srhmsubclem1  20840  srhmsubc  20843  isidom  20887  isfld  20904  isofld  21031  2idlelb  21456  qus1  21477  qusrhm  21479  lmres  23526  isnvc  24922  cvslvec  25354  cvsclm  25355  iscvs  25356  cvsi  25359  ishl  25591  ply1pid  26409  rplogsum  27764  ltsres  27899  iscusgr  29879  isphg  31299  ishlo  31369  hhsscms  31760  mayete3i  32210  bj-elid6  37923  bj-isrvec  38047  caures  38511  iscrngo  38747  fldcrngo  38755  isdmn  38805  isolat  40086  srhmsubcALTV  49241  isidom2  49260