Theorem elin2d 4158

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-in 3912

This theorem is referenced by:  f1opwfi  9265  elfiun  9339  ordtypelem3  9431  infpwfien  9975  ttukeylem6  10427  fpwwe2lem11  10554  explecnv  15791  bitsinv1  16372  smuval2  16412  firest  17355  sscres  17749  funcres2c  17829  coffth  17864  rescfth  17865  catcoppccl  18043  catcfuccl  18044  catcxpccl  18132  psssdm2  18506  sylow2a  19517  frgpnabllem2  19772  idomdomd  20630  sralmod  21110  2idlridld  21181  zringlpirlem3  21390  mplind  21994  neiptoptop  23035  restbas  23062  ordtrest  23106  subbascn  23158  lmss  23202  cnconn  23326  clsconn  23334  conncompclo  23339  subislly  23385  cldllycmp  23399  1stckgenlem  23457  txcls  23508  txcnp  23524  txtube  23544  txcmplem1  23545  txkgen  23556  xkopt  23559  xkococnlem  23563  txconn  23593  basqtop  23615  tgqtop  23616  kqnrmlem1  23647  kqnrmlem2  23648  nrmhmph  23698  uzrest  23801  alexsubALTlem3  23953  ptcmplem2  23957  tsmslem1  24033  tsmsxplem1  24057  tsmsxplem2  24058  tsmsxp  24059  blin2  24334  met2ndci  24427  zdis  24722  reconnlem2  24733  reconn  24734  xrge0gsumle  24739  cnheibor  24871  lebnum  24880  nmoleub2lem3  25032  nmoleub3  25036  caussi  25214  minveclem4b  25348  minveclem4  25349  ovolfcl  25384  ovolfioo  25385  ovolficc  25386  ovolficcss  25387  ovolfsval  25388  ovoliunlem1  25420  ovolicc2lem4  25438  ovolicc2lem5  25439  uniiccdif  25496  uniioovol  25497  uniiccvol  25498  uniioombllem2a  25500  uniioombllem3a  25502  uniioombllem4  25504  uniioombllem5  25505  uniioombllem6  25506  vitalilem2  25527  vitalilem4  25529  ig1peu  26097  taylfvallem1  26281  tayl0  26286  ppisval  27031  chtf  27035  efchtcl  27038  chtge0  27039  ppinprm  27079  chtprm  27080  chtnprm  27081  chtwordi  27083  chtdif  27085  efchtdvds  27086  chtlepsi  27134  chtleppi  27138  pclogsum  27143  chpval2  27146  chpchtsum  27147  chpub  27148  chebbnd1lem1  27397  chtppilimlem1  27401  rplogsumlem2  27413  perpneq  28678  ragperp  28681  tocyc01  33079  cyc3evpm  33111  cycpmconjslem2  33116  cyc3conja  33118  ssdifidlprm  33414  mxidlirred  33428  pidufd  33499  1arithufdlem4  33503  ressdeg1  33520  exsslsb  33582  lbsdiflsp0  33612  irngss  33673  rtelextdg2lem  33712  esum2d  34079  ispisys2  34139  sigapisys  34141  sigapildsyslem  34147  sigapildsys  34148  sseqf  34379  tgoldbachgt  34650  bnj1172  34987  weiunfrlem  36457  mhpind  42587  ismnushort  44294  cnrefiisplem  45830  hoiqssbllem3  46625  smflimlem3  46774  iinfconstbas  49071  ffthoppf  49170  fucoppc  49415  termcterm  49518  termcterm2  49519