Theorem elin2 4155

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ∩ cin 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908

This theorem is referenced by:  elin3  4158  opelres  5944  elpredgg  6272  fnres  6619  funfvima  7176  fnwelem  8073  ressuppssdif  8127  fz1isolem  14384  isabl  19713  isogrp  20053  srhmsubclem1  20610  srhmsubc  20613  isidom  20658  isfld  20673  isofld  20797  2idlelb  21208  qus1  21229  qusrhm  21231  lmres  23244  isnvc  24639  cvslvec  25081  cvsclm  25082  iscvs  25083  cvsi  25086  ishl  25318  ply1pid  26144  rplogsum  27494  ltsres  27630  iscusgr  29491  isphg  30892  ishlo  30962  hhsscms  31353  mayete3i  31803  bj-elid6  37375  bj-isrvec  37499  caures  37961  iscrngo  38197  fldcrngo  38205  isdmn  38255  isolat  39472  srhmsubcALTV  48571