Theorem elin2d 4179

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

Syntax hints:   → wi 4   ∈ wcel 2113   ∩ cin 3938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-v 3499  df-in 3946

This theorem is referenced by:  f1opwfi  8831  elfiun  8897  ordtypelem3  8987  infpwfien  9491  ttukeylem6  9939  fpwwe2lem12  10066  explecnv  15223  bitsinv1  15794  smuval2  15834  firest  16709  sscres  17096  funcres2c  17174  coffth  17209  rescfth  17210  catcoppccl  17371  catcfuccl  17372  catcxpccl  17460  psssdm2  17828  frgpnabllem2  18997  sralmod  19962  mplind  20285  zringlpirlem3  20636  neiptoptop  21742  restbas  21769  ordtrest  21813  subbascn  21865  lmss  21909  cnconn  22033  clsconn  22041  conncompclo  22046  subislly  22092  cldllycmp  22106  1stckgenlem  22164  txcls  22215  txcnp  22231  txtube  22251  txcmplem1  22252  txkgen  22263  xkopt  22266  xkococnlem  22270  txconn  22300  basqtop  22322  tgqtop  22323  kqnrmlem1  22354  kqnrmlem2  22355  nrmhmph  22405  uzrest  22508  alexsubALTlem3  22660  ptcmplem2  22664  tsmslem1  22740  tsmsxplem1  22764  tsmsxplem2  22765  tsmsxp  22766  blin2  23042  met2ndci  23135  zdis  23427  reconnlem2  23438  reconn  23439  xrge0gsumle  23444  cnheibor  23562  lebnum  23571  nmoleub2lem3  23722  nmoleub3  23726  caussi  23903  minveclem4b  24037  minveclem4  24038  ovolfcl  24070  ovolfioo  24071  ovolficc  24072  ovolficcss  24073  ovolfsval  24074  ovoliunlem1  24106  ovolicc2lem4  24124  ovolicc2lem5  24125  uniiccdif  24182  uniioovol  24183  uniiccvol  24184  uniioombllem2a  24186  uniioombllem3a  24188  uniioombllem4  24190  uniioombllem5  24191  uniioombllem6  24192  vitalilem2  24213  vitalilem4  24215  ig1peu  24768  taylfvallem1  24948  tayl0  24953  ppisval  25684  chtf  25688  efchtcl  25691  chtge0  25692  ppinprm  25732  chtprm  25733  chtnprm  25734  chtwordi  25736  chtdif  25738  efchtdvds  25739  chtlepsi  25785  chtleppi  25789  pclogsum  25794  chpval2  25797  chpchtsum  25798  chpub  25799  chebbnd1lem1  26048  chtppilimlem1  26052  rplogsumlem2  26064  perpneq  26503  ragperp  26506  tocyc01  30764  cyc3evpm  30796  cycpmconjslem2  30801  cyc3conja  30803  lbsdiflsp0  31026  esum2d  31356  ispisys2  31416  sigapisys  31418  sigapildsyslem  31424  sigapildsys  31425  sseqf  31654  tgoldbachgt  31938  bnj1172  32277  cnrefiisplem  42116  hoiqssbllem3  42913  smflimlem3  43056