Theorem elin2d 4129

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

Syntax hints:   → wi 4   ∈ wcel 2108   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890

This theorem is referenced by:  f1opwfi  9053  elfiun  9119  ordtypelem3  9209  infpwfien  9749  ttukeylem6  10201  fpwwe2lem11  10328  explecnv  15505  bitsinv1  16077  smuval2  16117  firest  17060  sscres  17452  funcres2c  17533  coffth  17568  rescfth  17569  catcoppccl  17748  catcoppcclOLD  17749  catcfuccl  17750  catcfucclOLD  17751  catcxpccl  17840  catcxpcclOLD  17841  psssdm2  18214  sylow2a  19139  frgpnabllem2  19390  sralmod  20370  zringlpirlem3  20598  mplind  21188  neiptoptop  22190  restbas  22217  ordtrest  22261  subbascn  22313  lmss  22357  cnconn  22481  clsconn  22489  conncompclo  22494  subislly  22540  cldllycmp  22554  1stckgenlem  22612  txcls  22663  txcnp  22679  txtube  22699  txcmplem1  22700  txkgen  22711  xkopt  22714  xkococnlem  22718  txconn  22748  basqtop  22770  tgqtop  22771  kqnrmlem1  22802  kqnrmlem2  22803  nrmhmph  22853  uzrest  22956  alexsubALTlem3  23108  ptcmplem2  23112  tsmslem1  23188  tsmsxplem1  23212  tsmsxplem2  23213  tsmsxp  23214  blin2  23490  met2ndci  23584  zdis  23885  reconnlem2  23896  reconn  23897  xrge0gsumle  23902  cnheibor  24024  lebnum  24033  nmoleub2lem3  24184  nmoleub3  24188  caussi  24366  minveclem4b  24500  minveclem4  24501  ovolfcl  24535  ovolfioo  24536  ovolficc  24537  ovolficcss  24538  ovolfsval  24539  ovoliunlem1  24571  ovolicc2lem4  24589  ovolicc2lem5  24590  uniiccdif  24647  uniioovol  24648  uniiccvol  24649  uniioombllem2a  24651  uniioombllem3a  24653  uniioombllem4  24655  uniioombllem5  24656  uniioombllem6  24657  vitalilem2  24678  vitalilem4  24680  ig1peu  25241  taylfvallem1  25421  tayl0  25426  ppisval  26158  chtf  26162  efchtcl  26165  chtge0  26166  ppinprm  26206  chtprm  26207  chtnprm  26208  chtwordi  26210  chtdif  26212  efchtdvds  26213  chtlepsi  26259  chtleppi  26263  pclogsum  26268  chpval2  26271  chpchtsum  26272  chpub  26273  chebbnd1lem1  26522  chtppilimlem1  26526  rplogsumlem2  26538  perpneq  26979  ragperp  26982  tocyc01  31287  cyc3evpm  31319  cycpmconjslem2  31324  cyc3conja  31326  lbsdiflsp0  31609  esum2d  31961  ispisys2  32021  sigapisys  32023  sigapildsyslem  32029  sigapildsys  32030  sseqf  32259  tgoldbachgt  32543  bnj1172  32881  mhpind  40206  ismnushort  41808  cnrefiisplem  43260  hoiqssbllem3  44052  smflimlem3  44195