Theorem elin2d 4159

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

Syntax hints:   → wi 4   ∈ wcel 2114   ∩ cin 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-in 3910

This theorem is referenced by:  f1opwfi  9268  elfiun  9345  ordtypelem3  9437  infpwfien  9984  ttukeylem6  10436  fpwwe2lem11  10564  explecnv  15800  bitsinv1  16381  smuval2  16421  firest  17364  sscres  17759  funcres2c  17839  coffth  17874  rescfth  17875  catcoppccl  18053  catcfuccl  18054  catcxpccl  18142  psssdm2  18516  sylow2a  19560  frgpnabllem2  19815  idomdomd  20671  sralmod  21151  2idlridld  21222  zringlpirlem3  21431  mplind  22037  neiptoptop  23087  restbas  23114  ordtrest  23158  subbascn  23210  lmss  23254  cnconn  23378  clsconn  23386  conncompclo  23391  subislly  23437  cldllycmp  23451  1stckgenlem  23509  txcls  23560  txcnp  23576  txtube  23596  txcmplem1  23597  txkgen  23608  xkopt  23611  xkococnlem  23615  txconn  23645  basqtop  23667  tgqtop  23668  kqnrmlem1  23699  kqnrmlem2  23700  nrmhmph  23750  uzrest  23853  alexsubALTlem3  24005  ptcmplem2  24009  tsmslem1  24085  tsmsxplem1  24109  tsmsxplem2  24110  tsmsxp  24111  blin2  24385  met2ndci  24478  zdis  24773  reconnlem2  24784  reconn  24785  xrge0gsumle  24790  cnheibor  24922  lebnum  24931  nmoleub2lem3  25083  nmoleub3  25087  caussi  25265  minveclem4b  25399  minveclem4  25400  ovolfcl  25435  ovolfioo  25436  ovolficc  25437  ovolficcss  25438  ovolfsval  25439  ovoliunlem1  25471  ovolicc2lem4  25489  ovolicc2lem5  25490  uniiccdif  25547  uniioovol  25548  uniiccvol  25549  uniioombllem2a  25551  uniioombllem3a  25553  uniioombllem4  25555  uniioombllem5  25556  uniioombllem6  25557  vitalilem2  25578  vitalilem4  25580  ig1peu  26148  taylfvallem1  26332  tayl0  26337  ppisval  27082  chtf  27086  efchtcl  27089  chtge0  27090  ppinprm  27130  chtprm  27131  chtnprm  27132  chtwordi  27134  chtdif  27136  efchtdvds  27137  chtlepsi  27185  chtleppi  27189  pclogsum  27194  chpval2  27197  chpchtsum  27198  chpub  27199  chebbnd1lem1  27448  chtppilimlem1  27452  rplogsumlem2  27464  perpneq  28798  ragperp  28801  tocyc01  33212  cyc3evpm  33244  cycpmconjslem2  33249  cyc3conja  33251  ssdifidlprm  33551  mxidlirred  33565  pidufd  33636  1arithufdlem4  33640  ressdeg1  33659  exsslsb  33774  lbsdiflsp0  33804  irngss  33865  rtelextdg2lem  33904  esum2d  34271  ispisys2  34331  sigapisys  34333  sigapildsyslem  34339  sigapildsys  34340  sseqf  34570  tgoldbachgt  34841  bnj1172  35177  weiunfrlem  36680  mhpind  42952  ismnushort  44657  cnrefiisplem  46187  hoiqssbllem3  46982  smflimlem3  47131  iinfconstbas  49425  ffthoppf  49524  fucoppc  49769  termcterm  49872  termcterm2  49873