Theorem elin2d 4067

Description: Elementhood in the first set of an intersection - deduction version. (Contributed by Thierry Arnoux, 3-May-2020.)

Hypothesis

Ref	Expression
elin1d.1	⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))

Assertion

Ref	Expression
elin2d	⊢ (𝜑 → 𝑋 ∈ 𝐵)

Proof of Theorem elin2d

Step	Hyp	Ref	Expression
1		elin1d.1	. 2 ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))
2		elinel2 4064	. 2 ⊢ (𝑋 ∈ (𝐴 ∩ 𝐵) → 𝑋 ∈ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝑋 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2051   ∩ cin 3830

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2752

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2761  df-cleq 2773  df-clel 2848  df-nfc 2920  df-v 3419  df-in 3838

This theorem is referenced by:  f1opwfi  8629  elfiun  8695  ordtypelem3  8785  infpwfien  9288  ttukeylem6  9740  fpwwe2lem12  9867  explecnv  15086  bitsinv1  15657  smuval2  15697  firest  16568  sscres  16963  funcres2c  17041  coffth  17076  rescfth  17077  catcoppccl  17238  catcfuccl  17239  catcxpccl  17327  psssdm2  17695  frgpnabllem2  18762  sralmod  19693  mplind  20007  zringlpirlem3  20350  neiptoptop  21458  restbas  21485  ordtrest  21529  subbascn  21581  lmss  21625  cnconn  21749  clsconn  21757  conncompclo  21762  subislly  21808  cldllycmp  21822  1stckgenlem  21880  txcls  21931  txcnp  21947  txtube  21967  txcmplem1  21968  txkgen  21979  xkopt  21982  xkococnlem  21986  txconn  22016  basqtop  22038  tgqtop  22039  kqnrmlem1  22070  kqnrmlem2  22071  nrmhmph  22121  uzrest  22224  alexsubALTlem3  22376  ptcmplem2  22380  tsmslem1  22455  tsmsxplem1  22479  tsmsxplem2  22480  tsmsxp  22481  blin2  22757  met2ndci  22850  zdis  23142  reconnlem2  23153  reconn  23154  xrge0gsumle  23159  cnheibor  23277  lebnum  23286  nmoleub2lem3  23437  nmoleub3  23441  caussi  23618  minveclem4b  23752  minveclem4  23753  ovolfcl  23785  ovolfioo  23786  ovolficc  23787  ovolficcss  23788  ovolfsval  23789  ovoliunlem1  23821  ovolicc2lem4  23839  ovolicc2lem5  23840  uniiccdif  23897  uniioovol  23898  uniiccvol  23899  uniioombllem2a  23901  uniioombllem3a  23903  uniioombllem4  23905  uniioombllem5  23906  uniioombllem6  23907  vitalilem2  23928  vitalilem4  23930  ig1peu  24483  taylfvallem1  24663  tayl0  24668  ppisval  25398  chtf  25402  efchtcl  25405  chtge0  25406  ppinprm  25446  chtprm  25447  chtnprm  25448  chtwordi  25450  chtdif  25452  efchtdvds  25453  chtlepsi  25499  chtleppi  25503  pclogsum  25508  chpval2  25511  chpchtsum  25512  chpub  25513  chebbnd1lem1  25762  chtppilimlem1  25766  rplogsumlem2  25778  perpneq  26217  ragperp  26220  cyc3evpm  30495  lbsdiflsp0  30683  esum2d  31028  ispisys2  31089  sigapisys  31091  sigapildsyslem  31097  sigapildsys  31098  sseqf  31328  tgoldbachgt  31614  bnj1172  31950  cnrefiisplem  41576  hoiqssbllem3  42372  smflimlem3  42515