Theorem elin2 3688

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 2535	. 2
3		elin 3686	. 2
4	2, 3	bitri 249	1

Syntax hints:  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  i^icin 3474

This theorem is referenced by:  elin3  3689  fnres  5702  funfvima  6147  fnwelem  6915  ressuppssdif  6940  fz1isolem  12510  isabl  16802  isfld  17405  2idlcpbl  17882  qus1  17883  qusrhm  17885  isidom  17953  lmres  19801  isnvc  21203  cvslvec  21606  cvsclm  21607  ishl  21802  ply1pid  22580  rplogsum  23712  isphg  25732  ishlo  25803  hhsscms  26195  mayete3i  26646  isogrp  27692  isofld  27792  elpredim  29256  elpred  29257  elpredg  29258  sltres  29424  nofulllem5  29466  caures  30253  iscrngo  30394  fldcrng  30401  isdmn  30451  srhmsubclem1  32881  srhmsubc  32884  srhmsubcOLDlem1  32900  srhmsubcOLD  32903  isolat  34937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482