Theorem elin2 4162

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-in 3918

This theorem is referenced by:  elin3  4165  opelres  5945  elpredgg  6275  fnres  6627  funfvima  7186  fnwelem  8087  ressuppssdif  8141  fz1isolem  14402  isabl  19690  srhmsubclem1  20562  srhmsubc  20565  isidom  20610  isfld  20625  2idlelb  21139  qus1  21160  qusrhm  21162  lmres  23163  isnvc  24559  cvslvec  25001  cvsclm  25002  iscvs  25003  cvsi  25006  ishl  25238  ply1pid  26064  rplogsum  27414  sltres  27550  iscusgr  29321  isphg  30719  ishlo  30789  hhsscms  31180  mayete3i  31630  isogrp  32989  isofld  33253  bj-elid6  37131  bj-isrvec  37255  caures  37727  iscrngo  37963  fldcrngo  37971  isdmn  38021  isolat  39178  srhmsubcALTV  48286