Theorem elin2d 4185

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

Syntax hints:   → wi 4   ∈ wcel 2109   ∩ cin 3930

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-in 3938

This theorem is referenced by:  f1opwfi  9373  elfiun  9447  ordtypelem3  9539  infpwfien  10081  ttukeylem6  10533  fpwwe2lem11  10660  explecnv  15886  bitsinv1  16466  smuval2  16506  firest  17451  sscres  17841  funcres2c  17921  coffth  17956  rescfth  17957  catcoppccl  18135  catcfuccl  18136  catcxpccl  18224  psssdm2  18596  sylow2a  19605  frgpnabllem2  19860  idomdomd  20691  sralmod  21150  2idlridld  21221  zringlpirlem3  21430  mplind  22033  neiptoptop  23074  restbas  23101  ordtrest  23145  subbascn  23197  lmss  23241  cnconn  23365  clsconn  23373  conncompclo  23378  subislly  23424  cldllycmp  23438  1stckgenlem  23496  txcls  23547  txcnp  23563  txtube  23583  txcmplem1  23584  txkgen  23595  xkopt  23598  xkococnlem  23602  txconn  23632  basqtop  23654  tgqtop  23655  kqnrmlem1  23686  kqnrmlem2  23687  nrmhmph  23737  uzrest  23840  alexsubALTlem3  23992  ptcmplem2  23996  tsmslem1  24072  tsmsxplem1  24096  tsmsxplem2  24097  tsmsxp  24098  blin2  24373  met2ndci  24466  zdis  24761  reconnlem2  24772  reconn  24773  xrge0gsumle  24778  cnheibor  24910  lebnum  24919  nmoleub2lem3  25071  nmoleub3  25075  caussi  25254  minveclem4b  25388  minveclem4  25389  ovolfcl  25424  ovolfioo  25425  ovolficc  25426  ovolficcss  25427  ovolfsval  25428  ovoliunlem1  25460  ovolicc2lem4  25478  ovolicc2lem5  25479  uniiccdif  25536  uniioovol  25537  uniiccvol  25538  uniioombllem2a  25540  uniioombllem3a  25542  uniioombllem4  25544  uniioombllem5  25545  uniioombllem6  25546  vitalilem2  25567  vitalilem4  25569  ig1peu  26137  taylfvallem1  26321  tayl0  26326  ppisval  27071  chtf  27075  efchtcl  27078  chtge0  27079  ppinprm  27119  chtprm  27120  chtnprm  27121  chtwordi  27123  chtdif  27125  efchtdvds  27126  chtlepsi  27174  chtleppi  27178  pclogsum  27183  chpval2  27186  chpchtsum  27187  chpub  27188  chebbnd1lem1  27437  chtppilimlem1  27441  rplogsumlem2  27453  perpneq  28698  ragperp  28701  tocyc01  33134  cyc3evpm  33166  cycpmconjslem2  33171  cyc3conja  33173  ssdifidlprm  33478  mxidlirred  33492  pidufd  33563  1arithufdlem4  33567  ressdeg1  33584  exsslsb  33641  lbsdiflsp0  33671  irngss  33733  rtelextdg2lem  33765  esum2d  34129  ispisys2  34189  sigapisys  34191  sigapildsyslem  34197  sigapildsys  34198  sseqf  34429  tgoldbachgt  34700  bnj1172  35037  weiunfrlem  36487  mhpind  42592  ismnushort  44300  cnrefiisplem  45838  hoiqssbllem3  46633  smflimlem3  46782  iinfconstbas  49013  termcterm  49378  termcterm2  49379