Theorem elin2d 4113

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

Syntax hints:   → wi 4   ∈ wcel 2110   ∩ cin 3865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873

This theorem is referenced by:  f1opwfi  8980  elfiun  9046  ordtypelem3  9136  infpwfien  9676  ttukeylem6  10128  fpwwe2lem11  10255  explecnv  15429  bitsinv1  16001  smuval2  16041  firest  16937  sscres  17328  funcres2c  17408  coffth  17443  rescfth  17444  catcoppccl  17623  catcoppcclOLD  17624  catcfuccl  17625  catcfucclOLD  17626  catcxpccl  17714  catcxpcclOLD  17715  psssdm2  18087  sylow2a  19008  frgpnabllem2  19259  sralmod  20224  zringlpirlem3  20451  mplind  21028  neiptoptop  22028  restbas  22055  ordtrest  22099  subbascn  22151  lmss  22195  cnconn  22319  clsconn  22327  conncompclo  22332  subislly  22378  cldllycmp  22392  1stckgenlem  22450  txcls  22501  txcnp  22517  txtube  22537  txcmplem1  22538  txkgen  22549  xkopt  22552  xkococnlem  22556  txconn  22586  basqtop  22608  tgqtop  22609  kqnrmlem1  22640  kqnrmlem2  22641  nrmhmph  22691  uzrest  22794  alexsubALTlem3  22946  ptcmplem2  22950  tsmslem1  23026  tsmsxplem1  23050  tsmsxplem2  23051  tsmsxp  23052  blin2  23327  met2ndci  23420  zdis  23713  reconnlem2  23724  reconn  23725  xrge0gsumle  23730  cnheibor  23852  lebnum  23861  nmoleub2lem3  24012  nmoleub3  24016  caussi  24194  minveclem4b  24328  minveclem4  24329  ovolfcl  24363  ovolfioo  24364  ovolficc  24365  ovolficcss  24366  ovolfsval  24367  ovoliunlem1  24399  ovolicc2lem4  24417  ovolicc2lem5  24418  uniiccdif  24475  uniioovol  24476  uniiccvol  24477  uniioombllem2a  24479  uniioombllem3a  24481  uniioombllem4  24483  uniioombllem5  24484  uniioombllem6  24485  vitalilem2  24506  vitalilem4  24508  ig1peu  25069  taylfvallem1  25249  tayl0  25254  ppisval  25986  chtf  25990  efchtcl  25993  chtge0  25994  ppinprm  26034  chtprm  26035  chtnprm  26036  chtwordi  26038  chtdif  26040  efchtdvds  26041  chtlepsi  26087  chtleppi  26091  pclogsum  26096  chpval2  26099  chpchtsum  26100  chpub  26101  chebbnd1lem1  26350  chtppilimlem1  26354  rplogsumlem2  26366  perpneq  26805  ragperp  26808  tocyc01  31104  cyc3evpm  31136  cycpmconjslem2  31141  cyc3conja  31143  lbsdiflsp0  31421  esum2d  31773  ispisys2  31833  sigapisys  31835  sigapildsyslem  31841  sigapildsys  31842  sseqf  32071  tgoldbachgt  32355  bnj1172  32694  mhpind  39993  ismnushort  41592  cnrefiisplem  43045  hoiqssbllem3  43837  smflimlem3  43980