Theorem elin2d 4145

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3443  df-in 3904

This theorem is referenced by:  f1opwfi  9213  elfiun  9279  ordtypelem3  9369  infpwfien  9911  ttukeylem6  10363  fpwwe2lem11  10490  explecnv  15668  bitsinv1  16240  smuval2  16280  firest  17232  sscres  17624  funcres2c  17706  coffth  17741  rescfth  17742  catcoppccl  17921  catcoppcclOLD  17922  catcfuccl  17923  catcfucclOLD  17924  catcxpccl  18013  catcxpcclOLD  18014  psssdm2  18388  sylow2a  19312  frgpnabllem2  19562  sralmod  20555  zringlpirlem3  20784  mplind  21376  neiptoptop  22380  restbas  22407  ordtrest  22451  subbascn  22503  lmss  22547  cnconn  22671  clsconn  22679  conncompclo  22684  subislly  22730  cldllycmp  22744  1stckgenlem  22802  txcls  22853  txcnp  22869  txtube  22889  txcmplem1  22890  txkgen  22901  xkopt  22904  xkococnlem  22908  txconn  22938  basqtop  22960  tgqtop  22961  kqnrmlem1  22992  kqnrmlem2  22993  nrmhmph  23043  uzrest  23146  alexsubALTlem3  23298  ptcmplem2  23302  tsmslem1  23378  tsmsxplem1  23402  tsmsxplem2  23403  tsmsxp  23404  blin2  23680  met2ndci  23776  zdis  24077  reconnlem2  24088  reconn  24089  xrge0gsumle  24094  cnheibor  24216  lebnum  24225  nmoleub2lem3  24376  nmoleub3  24380  caussi  24559  minveclem4b  24693  minveclem4  24694  ovolfcl  24728  ovolfioo  24729  ovolficc  24730  ovolficcss  24731  ovolfsval  24732  ovoliunlem1  24764  ovolicc2lem4  24782  ovolicc2lem5  24783  uniiccdif  24840  uniioovol  24841  uniiccvol  24842  uniioombllem2a  24844  uniioombllem3a  24846  uniioombllem4  24848  uniioombllem5  24849  uniioombllem6  24850  vitalilem2  24871  vitalilem4  24873  ig1peu  25434  taylfvallem1  25614  tayl0  25619  ppisval  26351  chtf  26355  efchtcl  26358  chtge0  26359  ppinprm  26399  chtprm  26400  chtnprm  26401  chtwordi  26403  chtdif  26405  efchtdvds  26406  chtlepsi  26452  chtleppi  26456  pclogsum  26461  chpval2  26464  chpchtsum  26465  chpub  26466  chebbnd1lem1  26715  chtppilimlem1  26719  rplogsumlem2  26731  perpneq  27305  ragperp  27308  tocyc01  31613  cyc3evpm  31645  cycpmconjslem2  31650  cyc3conja  31652  lbsdiflsp0  31946  esum2d  32300  ispisys2  32360  sigapisys  32362  sigapildsyslem  32368  sigapildsys  32369  sseqf  32600  tgoldbachgt  32884  bnj1172  33221  mhpind  40533  ismnushort  42229  cnrefiisplem  43695  hoiqssbllem3  44488  smflimlem3  44637