Theorem elin2d 4214

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

Syntax hints:   → wi 4   ∈ wcel 2105   ∩ cin 3961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-in 3969

This theorem is referenced by:  f1opwfi  9393  elfiun  9467  ordtypelem3  9557  infpwfien  10099  ttukeylem6  10551  fpwwe2lem11  10678  explecnv  15897  bitsinv1  16475  smuval2  16515  firest  17478  sscres  17870  funcres2c  17954  coffth  17989  rescfth  17990  catcoppccl  18170  catcoppcclOLD  18171  catcfuccl  18172  catcfucclOLD  18173  catcxpccl  18262  catcxpcclOLD  18263  psssdm2  18638  sylow2a  19651  frgpnabllem2  19906  idomdomd  20742  sralmod  21211  2idlridld  21282  zringlpirlem3  21492  mplind  22111  neiptoptop  23154  restbas  23181  ordtrest  23225  subbascn  23277  lmss  23321  cnconn  23445  clsconn  23453  conncompclo  23458  subislly  23504  cldllycmp  23518  1stckgenlem  23576  txcls  23627  txcnp  23643  txtube  23663  txcmplem1  23664  txkgen  23675  xkopt  23678  xkococnlem  23682  txconn  23712  basqtop  23734  tgqtop  23735  kqnrmlem1  23766  kqnrmlem2  23767  nrmhmph  23817  uzrest  23920  alexsubALTlem3  24072  ptcmplem2  24076  tsmslem1  24152  tsmsxplem1  24176  tsmsxplem2  24177  tsmsxp  24178  blin2  24454  met2ndci  24550  zdis  24851  reconnlem2  24862  reconn  24863  xrge0gsumle  24868  cnheibor  25000  lebnum  25009  nmoleub2lem3  25161  nmoleub3  25165  caussi  25344  minveclem4b  25478  minveclem4  25479  ovolfcl  25514  ovolfioo  25515  ovolficc  25516  ovolficcss  25517  ovolfsval  25518  ovoliunlem1  25550  ovolicc2lem4  25568  ovolicc2lem5  25569  uniiccdif  25626  uniioovol  25627  uniiccvol  25628  uniioombllem2a  25630  uniioombllem3a  25632  uniioombllem4  25634  uniioombllem5  25635  uniioombllem6  25636  vitalilem2  25657  vitalilem4  25659  ig1peu  26228  taylfvallem1  26412  tayl0  26417  ppisval  27161  chtf  27165  efchtcl  27168  chtge0  27169  ppinprm  27209  chtprm  27210  chtnprm  27211  chtwordi  27213  chtdif  27215  efchtdvds  27216  chtlepsi  27264  chtleppi  27268  pclogsum  27273  chpval2  27276  chpchtsum  27277  chpub  27278  chebbnd1lem1  27527  chtppilimlem1  27531  rplogsumlem2  27543  perpneq  28736  ragperp  28739  tocyc01  33120  cyc3evpm  33152  cycpmconjslem2  33157  cyc3conja  33159  ssdifidlprm  33465  mxidlirred  33479  pidufd  33550  1arithufdlem4  33554  ressdeg1  33570  lbsdiflsp0  33653  irngss  33701  rtelextdg2lem  33731  esum2d  34073  ispisys2  34133  sigapisys  34135  sigapildsyslem  34141  sigapildsys  34142  sseqf  34373  tgoldbachgt  34656  bnj1172  34993  weiunfrlem  36446  mhpind  42580  ismnushort  44296  cnrefiisplem  45784  hoiqssbllem3  46579  smflimlem3  46728