Theorem elin2d 4204

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 4201	. 2 ⊢ (𝑋 ∈ (𝐴 ∩ 𝐵) → 𝑋 ∈ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝑋 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2107   ∩ cin 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-in 3957

This theorem is referenced by:  f1opwfi  9397  elfiun  9471  ordtypelem3  9561  infpwfien  10103  ttukeylem6  10555  fpwwe2lem11  10682  explecnv  15902  bitsinv1  16480  smuval2  16520  firest  17478  sscres  17868  funcres2c  17949  coffth  17984  rescfth  17985  catcoppccl  18163  catcfuccl  18164  catcxpccl  18253  psssdm2  18627  sylow2a  19638  frgpnabllem2  19893  idomdomd  20727  sralmod  21195  2idlridld  21266  zringlpirlem3  21476  mplind  22095  neiptoptop  23140  restbas  23167  ordtrest  23211  subbascn  23263  lmss  23307  cnconn  23431  clsconn  23439  conncompclo  23444  subislly  23490  cldllycmp  23504  1stckgenlem  23562  txcls  23613  txcnp  23629  txtube  23649  txcmplem1  23650  txkgen  23661  xkopt  23664  xkococnlem  23668  txconn  23698  basqtop  23720  tgqtop  23721  kqnrmlem1  23752  kqnrmlem2  23753  nrmhmph  23803  uzrest  23906  alexsubALTlem3  24058  ptcmplem2  24062  tsmslem1  24138  tsmsxplem1  24162  tsmsxplem2  24163  tsmsxp  24164  blin2  24440  met2ndci  24536  zdis  24839  reconnlem2  24850  reconn  24851  xrge0gsumle  24856  cnheibor  24988  lebnum  24997  nmoleub2lem3  25149  nmoleub3  25153  caussi  25332  minveclem4b  25466  minveclem4  25467  ovolfcl  25502  ovolfioo  25503  ovolficc  25504  ovolficcss  25505  ovolfsval  25506  ovoliunlem1  25538  ovolicc2lem4  25556  ovolicc2lem5  25557  uniiccdif  25614  uniioovol  25615  uniiccvol  25616  uniioombllem2a  25618  uniioombllem3a  25620  uniioombllem4  25622  uniioombllem5  25623  uniioombllem6  25624  vitalilem2  25645  vitalilem4  25647  ig1peu  26215  taylfvallem1  26399  tayl0  26404  ppisval  27148  chtf  27152  efchtcl  27155  chtge0  27156  ppinprm  27196  chtprm  27197  chtnprm  27198  chtwordi  27200  chtdif  27202  efchtdvds  27203  chtlepsi  27251  chtleppi  27255  pclogsum  27260  chpval2  27263  chpchtsum  27264  chpub  27265  chebbnd1lem1  27514  chtppilimlem1  27518  rplogsumlem2  27530  perpneq  28723  ragperp  28726  tocyc01  33139  cyc3evpm  33171  cycpmconjslem2  33176  cyc3conja  33178  ssdifidlprm  33487  mxidlirred  33501  pidufd  33572  1arithufdlem4  33576  ressdeg1  33592  exsslsb  33648  lbsdiflsp0  33678  irngss  33738  rtelextdg2lem  33768  esum2d  34095  ispisys2  34155  sigapisys  34157  sigapildsyslem  34163  sigapildsys  34164  sseqf  34395  tgoldbachgt  34679  bnj1172  35016  weiunfrlem  36466  mhpind  42609  ismnushort  44325  cnrefiisplem  45849  hoiqssbllem3  46644  smflimlem3  46793  termcterm  49173  termcterm2  49174