Theorem elin2 4099

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

Syntax hints:   ↔ wb 207   ∧ wa 396   = wceq 1522   ∈ wcel 2081   ∩ cin 3862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-v 3439  df-in 3870

This theorem is referenced by:  elin3  4102  opelres  5745  elpredim  6040  elpred  6041  elpredg  6042  fnres  6349  funfvima  6863  fnwelem  7683  ressuppssdif  7707  fz1isolem  13672  isabl  18642  isfld  19206  2idlcpbl  19701  qus1  19702  qusrhm  19704  isidom  19771  lmres  21597  isnvc  22992  cvslvec  23417  cvsclm  23418  iscvs  23419  cvsi  23422  ishl  23653  ply1pid  24461  rplogsum  25790  iscusgr  26888  isphg  28290  ishlo  28360  hhsscms  28751  mayete3i  29201  isogrp  30368  isofld  30534  sltres  32784  caures  34592  iscrngo  34831  fldcrng  34839  isdmn  34889  isolat  35904  srhmsubclem1  43848  srhmsubc  43851  srhmsubcALTV  43869