Theorem elin2d 4166

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

Syntax hints:   → wi 4   ∈ wcel 2149   ∩ cin 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-in 3920

This theorem is referenced by:  f1opwfi  9309  elfiun  9386  ordtypelem3  9478  infpwfien  10042  ttukeylem6  10494  fpwwe2lem11  10622  explecnv  15915  bitsinv1  16496  smuval2  16536  firest  17481  sscres  17876  funcres2c  17956  coffth  17991  rescfth  17992  catcoppccl  18170  catcfuccl  18171  catcxpccl  18259  psssdm2  18633  sylow2a  19685  frgpnabllem2  19940  idomdomd  20806  sralmod  21282  2idlridld  21361  ssdifidlprm  21451  zringlpirlem3  21579  mplind  22186  neiptoptop  23253  restbas  23280  ordtrest  23324  subbascn  23376  lmss  23420  cnconn  23544  clsconn  23552  conncompclo  23557  subislly  23603  cldllycmp  23617  1stckgenlem  23675  txcls  23726  txcnp  23742  txtube  23762  txcmplem1  23763  txkgen  23774  xkopt  23777  xkococnlem  23781  txconn  23811  basqtop  23833  tgqtop  23834  kqnrmlem1  23865  kqnrmlem2  23866  nrmhmph  23916  uzrest  24019  alexsubALTlem3  24171  ptcmplem2  24175  tsmslem1  24251  tsmsxplem1  24275  tsmsxplem2  24276  tsmsxp  24277  blin2  24551  met2ndci  24644  zdis  24939  reconnlem2  24950  reconn  24951  xrge0gsumle  24956  cnheibor  25079  lebnum  25088  nmoleub2lem3  25239  nmoleub3  25243  caussi  25421  minveclem4b  25555  minveclem4  25556  ovolfcl  25590  ovolfioo  25591  ovolficc  25592  ovolficcss  25593  ovolfsval  25594  ovoliunlem1  25626  ovolicc2lem4  25644  ovolicc2lem5  25645  uniiccdif  25702  uniioovol  25703  uniiccvol  25704  uniioombllem2a  25706  uniioombllem3a  25708  uniioombllem4  25710  uniioombllem5  25711  uniioombllem6  25712  vitalilem2  25733  vitalilem4  25735  ig1peu  26297  taylfvallem1  26482  tayl0  26487  ppisval  27230  chtf  27234  efchtcl  27237  chtge0  27238  ppinprm  27278  chtprm  27279  chtnprm  27280  chtwordi  27282  chtdif  27284  efchtdvds  27285  chtlepsi  27332  chtleppi  27336  pclogsum  27341  chpval2  27344  chpchtsum  27345  chpub  27346  chebbnd1lem1  27595  chtppilimlem1  27599  rplogsumlem2  27611  tglnpt4  28886  perpneq  28949  ragperp  28952  lnincplng  29020  perpprlng  29149  tocyc01  33375  cyc3evpm  33407  cycpmconjslem2  33412  cyc3conja  33414  mxidlirred  33696  dflringlem3  33727  dflring4  33729  pidufd  33774  1arithufdlem4  33778  ressdeg1  33797  exsslsb  33928  lbsdiflsp0  33957  irngss  34018  rtelextdg2lem  34057  esum2d  34424  ispisys2  34484  sigapisys  34486  sigapildsyslem  34492  sigapildsys  34493  sseqf  34723  tgoldbachgt  34991  bnj1172  35330  weiunfrlem  36860  dfttc4  36926  mhpind  43213  ismnushort  44898  cnrefiisplem  46430  hoiqssbllem3  47225  sssmf  47339  smflimlem3  47374  iinfconstbas  49724  ffthoppf  49823  fucoppc  50068  termcterm  50171  termcterm2  50172