Theorem elin2 4143

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ∩ cin 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-in 3896

This theorem is referenced by:  elin3  4146  opelres  5950  elpredgg  6278  fnres  6625  funfvima  7185  fnwelem  8081  ressuppssdif  8135  fz1isolem  14423  isabl  19759  isogrp  20099  srhmsubclem1  20654  srhmsubc  20657  isidom  20702  isfld  20717  isofld  20841  2idlelb  21251  qus1  21272  qusrhm  21274  lmres  23265  isnvc  24660  cvslvec  25092  cvsclm  25093  iscvs  25094  cvsi  25097  ishl  25329  ply1pid  26148  rplogsum  27490  ltsres  27626  iscusgr  29487  isphg  30888  ishlo  30958  hhsscms  31349  mayete3i  31799  bj-elid6  37484  bj-isrvec  37608  caures  38081  iscrngo  38317  fldcrngo  38325  isdmn  38375  isolat  39658  srhmsubcALTV  48801