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

Syntax hints:   ↔ wb 208   ∧ wa 399   = wceq 1560   ∈ wcel 2142   ∩ cin 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-in 3911

This theorem is referenced by:  elin3  4158  opelres  5971  elpredgg  6301  fnres  6648  funfvima  7214  fnwelem  8111  ressuppssdif  8165  fz1isolem  14474  isabl  19824  isogrp  20164  srhmsubclem1  20727  srhmsubc  20730  isidom  20775  isfld  20790  isofld  20913  2idlelb  21323  qus1  21344  qusrhm  21346  lmres  23360  isnvc  24755  cvslvec  25187  cvsclm  25188  iscvs  25189  cvsi  25192  ishl  25424  ply1pid  26243  rplogsum  27591  ltsres  27726  iscusgr  29619  isphg  31020  ishlo  31090  hhsscms  31481  mayete3i  31931  bj-elid6  37662  bj-isrvec  37786  caures  38259  iscrngo  38495  fldcrngo  38503  isdmn  38553  isolat  39836  srhmsubcALTV  48947