Theorem elin2d 4158

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ∩ cin 3905

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3913

This theorem is used by:  f1opwfi  9316  elfiun  9393  ordtypelem3  9485  infpwfien  10058  ttukeylem6  10509  fpwwe2lem11  10637  explecnv  15938  bitsinv1  16518  smuval2  16558  firest  17503  sscres  17898  funcres2c  17978  coffth  18013  rescfth  18014  catcoppccl  18192  catcfuccl  18193  catcxpccl  18281  psssdm2  18655  sylow2a  19713  frgpnabllem2  19968  idomdomd  20854  sralmod  21338  2idlridld  21424  ssdifidlprm  21516  zringlpirlem3  21644  mplind  22251  neiptoptop  23318  restbas  23345  ordtrest  23389  subbascn  23441  lmss  23485  cnconn  23609  clsconn  23617  conncompclo  23622  subislly  23669  cldllycmp  23683  1stckgenlem  23741  txcls  23792  txcnp  23808  txtube  23828  txcmplem1  23829  txkgen  23840  xkopt  23843  xkococnlem  23847  txconn  23877  basqtop  23899  tgqtop  23900  kqnrmlem1  23931  kqnrmlem2  23932  nrmhmph  23982  uzrest  24085  alexsubALTlem3  24237  ptcmplem2  24241  tsmslem1  24317  tsmsxplem1  24341  tsmsxplem2  24342  tsmsxp  24343  blin2  24617  met2ndci  24710  zdis  25005  reconnlem2  25016  reconn  25017  xrge0gsumle  25022  cnheibor  25145  lebnum  25154  nmoleub2lem3  25305  nmoleub3  25309  caussi  25487  minveclem4b  25621  minveclem4  25622  ovolfcl  25656  ovolfioo  25657  ovolficc  25658  ovolficcss  25659  ovolfsval  25660  ovoliunlem1  25692  ovolicc2lem4  25710  ovolicc2lem5  25711  uniiccdif  25768  uniioovol  25769  uniiccvol  25770  uniioombllem2a  25772  uniioombllem3a  25774  uniioombllem4  25776  uniioombllem5  25777  uniioombllem6  25778  vitalilem2  25799  vitalilem4  25801  ig1peu  26363  taylfvallem1  26551  tayl0  26556  ppisval  27299  chtf  27303  efchtcl  27306  chtge0  27307  ppinprm  27347  chtprm  27348  chtnprm  27349  chtwordi  27351  chtdif  27353  efchtdvds  27354  chtlepsi  27401  chtleppi  27405  pclogsum  27410  chpval2  27413  chpchtsum  27414  chpub  27415  chebbnd1lem1  27664  chtppilimlem1  27668  rplogsumlem2  27680  tglnpt4  28959  perpneq  29025  ragperp  29028  lnincplng  29097  perpprlng  29231  prlngplngtr  29240  quadcgrprlng  29247  tocyc01  33478  cyc3evpm  33510  cycpmconjslem2  33515  cyc3conja  33517  mxidlirred  33795  dflringlem3  33826  dflring4  33828  pidufd  33873  1arithufdlem4  33877  ressdeg1  33896  exsslsb  34027  lbsdiflsp0  34056  irngss  34117  rtelextdg2lem  34156  esum2d  34523  ispisys2  34584  sigapisys  34586  sigapildsyslem  34592  sigapildsys  34593  sseqf  34823  tgoldbachgt  35091  bnj1172  35430  weiunfrlem  37008  dfttc4  37074  mhpind  43359  ismnushort  45044  cnrefiisplem  46576  hoiqssbllem3  47371  sssmf  47485  smflimlem3  47520  iinfconstbas  49877  ffthoppf  49976  fucoppc  50221  termcterm  50324  termcterm2  50325