Theorem elin2 4203

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958

This theorem is referenced by:  elin3  4206  opelres  6003  elpredgg  6334  fnres  6695  funfvima  7250  fnwelem  8156  ressuppssdif  8210  fz1isolem  14500  isabl  19802  srhmsubclem1  20677  srhmsubc  20680  isidom  20725  isfld  20740  2idlelb  21263  qus1  21284  qusrhm  21286  lmres  23308  isnvc  24716  cvslvec  25158  cvsclm  25159  iscvs  25160  cvsi  25163  ishl  25396  ply1pid  26222  rplogsum  27571  sltres  27707  iscusgr  29435  isphg  30836  ishlo  30906  hhsscms  31297  mayete3i  31747  isogrp  33079  isofld  33332  bj-elid6  37171  bj-isrvec  37295  caures  37767  iscrngo  38003  fldcrngo  38011  isdmn  38061  isolat  39213  srhmsubcALTV  48241