Theorem elin2 4226

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-in 3983

This theorem is referenced by:  elin3  4229  opelres  6015  elpredgg  6345  fnres  6707  funfvima  7267  fnwelem  8172  ressuppssdif  8226  fz1isolem  14510  isabl  19826  srhmsubclem1  20699  srhmsubc  20702  isidom  20747  isfld  20762  2idlelb  21286  qus1  21307  qusrhm  21309  lmres  23329  isnvc  24737  cvslvec  25177  cvsclm  25178  iscvs  25179  cvsi  25182  ishl  25415  ply1pid  26242  rplogsum  27589  sltres  27725  iscusgr  29453  isphg  30849  ishlo  30919  hhsscms  31310  mayete3i  31760  isogrp  33052  isofld  33297  bj-elid6  37136  bj-isrvec  37260  caures  37720  iscrngo  37956  fldcrngo  37964  isdmn  38014  isolat  39168  srhmsubcALTV  48048