Theorem elin2 3801

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

Syntax hints:   ↔ wb 196   ∧ wa 384   = wceq 1483   ∈ wcel 1990   ∩ cin 3573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581

This theorem is referenced by:  elin3  3804  elpredim  5692  elpred  5693  elpredg  5694  fnres  6007  funfvima  6492  fnwelem  7292  ressuppssdif  7316  fz1isolem  13245  isabl  18197  isfld  18756  2idlcpbl  19234  qus1  19235  qusrhm  19237  isidom  19304  lmres  21104  isnvc  22499  cvslvec  22925  cvsclm  22926  iscvs  22927  ishl  23158  ply1pid  23939  rplogsum  25216  isphg  27672  ishlo  27743  hhsscms  28136  mayete3i  28587  isogrp  29702  isofld  29802  sltres  31815  caures  33556  iscrngo  33795  fldcrng  33803  isdmn  33853  opelresALTV  34031  isolat  34499  srhmsubclem1  42073  srhmsubc  42076  srhmsubcALTV  42094