Theorem elin2d 4199

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

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

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 3473  df-in 3954

This theorem is referenced by:  f1opwfi  9381  elfiun  9454  ordtypelem3  9544  infpwfien  10086  ttukeylem6  10538  fpwwe2lem11  10665  explecnv  15844  bitsinv1  16417  smuval2  16457  firest  17414  sscres  17806  funcres2c  17890  coffth  17925  rescfth  17926  catcoppccl  18106  catcoppcclOLD  18107  catcfuccl  18108  catcfucclOLD  18109  catcxpccl  18198  catcxpcclOLD  18199  psssdm2  18573  sylow2a  19574  frgpnabllem2  19829  sralmod  21080  2idlridld  21149  idomdomd  21255  zringlpirlem3  21390  mplind  22014  neiptoptop  23048  restbas  23075  ordtrest  23119  subbascn  23171  lmss  23215  cnconn  23339  clsconn  23347  conncompclo  23352  subislly  23398  cldllycmp  23412  1stckgenlem  23470  txcls  23521  txcnp  23537  txtube  23557  txcmplem1  23558  txkgen  23569  xkopt  23572  xkococnlem  23576  txconn  23606  basqtop  23628  tgqtop  23629  kqnrmlem1  23660  kqnrmlem2  23661  nrmhmph  23711  uzrest  23814  alexsubALTlem3  23966  ptcmplem2  23970  tsmslem1  24046  tsmsxplem1  24070  tsmsxplem2  24071  tsmsxp  24072  blin2  24348  met2ndci  24444  zdis  24745  reconnlem2  24756  reconn  24757  xrge0gsumle  24762  cnheibor  24894  lebnum  24903  nmoleub2lem3  25055  nmoleub3  25059  caussi  25238  minveclem4b  25372  minveclem4  25373  ovolfcl  25408  ovolfioo  25409  ovolficc  25410  ovolficcss  25411  ovolfsval  25412  ovoliunlem1  25444  ovolicc2lem4  25462  ovolicc2lem5  25463  uniiccdif  25520  uniioovol  25521  uniiccvol  25522  uniioombllem2a  25524  uniioombllem3a  25526  uniioombllem4  25528  uniioombllem5  25529  uniioombllem6  25530  vitalilem2  25551  vitalilem4  25553  ig1peu  26122  taylfvallem1  26304  tayl0  26309  ppisval  27049  chtf  27053  efchtcl  27056  chtge0  27057  ppinprm  27097  chtprm  27098  chtnprm  27099  chtwordi  27101  chtdif  27103  efchtdvds  27104  chtlepsi  27152  chtleppi  27156  pclogsum  27161  chpval2  27164  chpchtsum  27165  chpub  27166  chebbnd1lem1  27415  chtppilimlem1  27419  rplogsumlem2  27431  perpneq  28531  ragperp  28534  tocyc01  32852  cyc3evpm  32884  cycpmconjslem2  32889  cyc3conja  32891  mxidlirred  33198  ressdeg1  33251  lbsdiflsp0  33324  irngss  33365  esum2d  33712  ispisys2  33772  sigapisys  33774  sigapildsyslem  33780  sigapildsys  33781  sseqf  34012  tgoldbachgt  34295  bnj1172  34632  mhpind  41827  ismnushort  43738  cnrefiisplem  45217  hoiqssbllem3  46012  smflimlem3  46161