Theorem elin2d 4196

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

Syntax hints:   → wi 4   ∈ wcel 2099   ∩ cin 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3472  df-in 3952

This theorem is referenced by:  f1opwfi  9375  elfiun  9448  ordtypelem3  9538  infpwfien  10080  ttukeylem6  10532  fpwwe2lem11  10659  explecnv  15838  bitsinv1  16411  smuval2  16451  firest  17408  sscres  17800  funcres2c  17884  coffth  17919  rescfth  17920  catcoppccl  18100  catcoppcclOLD  18101  catcfuccl  18102  catcfucclOLD  18103  catcxpccl  18192  catcxpcclOLD  18193  psssdm2  18567  sylow2a  19568  frgpnabllem2  19823  sralmod  21074  2idlridld  21143  idomdomd  21249  zringlpirlem3  21384  mplind  22008  neiptoptop  23029  restbas  23056  ordtrest  23100  subbascn  23152  lmss  23196  cnconn  23320  clsconn  23328  conncompclo  23333  subislly  23379  cldllycmp  23393  1stckgenlem  23451  txcls  23502  txcnp  23518  txtube  23538  txcmplem1  23539  txkgen  23550  xkopt  23553  xkococnlem  23557  txconn  23587  basqtop  23609  tgqtop  23610  kqnrmlem1  23641  kqnrmlem2  23642  nrmhmph  23692  uzrest  23795  alexsubALTlem3  23947  ptcmplem2  23951  tsmslem1  24027  tsmsxplem1  24051  tsmsxplem2  24052  tsmsxp  24053  blin2  24329  met2ndci  24425  zdis  24726  reconnlem2  24737  reconn  24738  xrge0gsumle  24743  cnheibor  24875  lebnum  24884  nmoleub2lem3  25036  nmoleub3  25040  caussi  25219  minveclem4b  25353  minveclem4  25354  ovolfcl  25389  ovolfioo  25390  ovolficc  25391  ovolficcss  25392  ovolfsval  25393  ovoliunlem1  25425  ovolicc2lem4  25443  ovolicc2lem5  25444  uniiccdif  25501  uniioovol  25502  uniiccvol  25503  uniioombllem2a  25505  uniioombllem3a  25507  uniioombllem4  25509  uniioombllem5  25510  uniioombllem6  25511  vitalilem2  25532  vitalilem4  25534  ig1peu  26103  taylfvallem1  26285  tayl0  26290  ppisval  27030  chtf  27034  efchtcl  27037  chtge0  27038  ppinprm  27078  chtprm  27079  chtnprm  27080  chtwordi  27082  chtdif  27084  efchtdvds  27085  chtlepsi  27133  chtleppi  27137  pclogsum  27142  chpval2  27145  chpchtsum  27146  chpub  27147  chebbnd1lem1  27396  chtppilimlem1  27400  rplogsumlem2  27412  perpneq  28512  ragperp  28515  tocyc01  32834  cyc3evpm  32866  cycpmconjslem2  32871  cyc3conja  32873  mxidlirred  33180  ressdeg1  33236  lbsdiflsp0  33315  irngss  33356  esum2d  33707  ispisys2  33767  sigapisys  33769  sigapildsyslem  33775  sigapildsys  33776  sseqf  34007  tgoldbachgt  34290  bnj1172  34627  mhpind  41818  ismnushort  43729  cnrefiisplem  45208  hoiqssbllem3  46003  smflimlem3  46152