Theorem elin2d 4155

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

Syntax hints:   → wi 4   ∈ wcel 2141   ∩ cin 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-in 3909

This theorem is referenced by:  f1opwfi  9293  elfiun  9370  ordtypelem3  9462  infpwfien  10012  ttukeylem6  10465  fpwwe2lem11  10593  explecnv  15886  bitsinv1  16467  smuval2  16507  firest  17452  sscres  17847  funcres2c  17927  coffth  17962  rescfth  17963  catcoppccl  18141  catcfuccl  18142  catcxpccl  18230  psssdm2  18604  sylow2a  19650  frgpnabllem2  19905  idomdomd  20763  sralmod  21242  2idlridld  21313  zringlpirlem3  21504  mplind  22111  neiptoptop  23179  restbas  23206  ordtrest  23250  subbascn  23302  lmss  23346  cnconn  23470  clsconn  23478  conncompclo  23483  subislly  23529  cldllycmp  23543  1stckgenlem  23601  txcls  23652  txcnp  23668  txtube  23688  txcmplem1  23689  txkgen  23700  xkopt  23703  xkococnlem  23707  txconn  23737  basqtop  23759  tgqtop  23760  kqnrmlem1  23791  kqnrmlem2  23792  nrmhmph  23842  uzrest  23945  alexsubALTlem3  24097  ptcmplem2  24101  tsmslem1  24177  tsmsxplem1  24201  tsmsxplem2  24202  tsmsxp  24203  blin2  24477  met2ndci  24570  zdis  24865  reconnlem2  24876  reconn  24877  xrge0gsumle  24882  cnheibor  25005  lebnum  25014  nmoleub2lem3  25165  nmoleub3  25169  caussi  25347  minveclem4b  25481  minveclem4  25482  ovolfcl  25516  ovolfioo  25517  ovolficc  25518  ovolficcss  25519  ovolfsval  25520  ovoliunlem1  25552  ovolicc2lem4  25570  ovolicc2lem5  25571  uniiccdif  25628  uniioovol  25629  uniiccvol  25630  uniioombllem2a  25632  uniioombllem3a  25634  uniioombllem4  25636  uniioombllem5  25637  uniioombllem6  25638  vitalilem2  25659  vitalilem4  25661  ig1peu  26223  taylfvallem1  26408  tayl0  26413  ppisval  27156  chtf  27160  efchtcl  27163  chtge0  27164  ppinprm  27204  chtprm  27205  chtnprm  27206  chtwordi  27208  chtdif  27210  efchtdvds  27211  chtlepsi  27258  chtleppi  27262  pclogsum  27267  chpval2  27270  chpchtsum  27271  chpub  27272  chebbnd1lem1  27521  chtppilimlem1  27525  rplogsumlem2  27537  perpneq  28871  ragperp  28874  tocyc01  33259  cyc3evpm  33291  cycpmconjslem2  33296  cyc3conja  33298  ssdifidlprm  33606  mxidlirred  33621  dflringlem3  33653  dflring4  33655  pidufd  33700  1arithufdlem4  33704  ressdeg1  33723  exsslsb  33855  lbsdiflsp0  33884  irngss  33945  rtelextdg2lem  33984  esum2d  34351  ispisys2  34411  sigapisys  34413  sigapildsyslem  34419  sigapildsys  34420  sseqf  34650  tgoldbachgt  34918  bnj1172  35257  weiunfrlem  36785  dfttc4  36851  mhpind  43137  ismnushort  44838  cnrefiisplem  46364  hoiqssbllem3  47159  sssmf  47273  smflimlem3  47308  iinfconstbas  49648  ffthoppf  49747  fucoppc  49992  termcterm  50095  termcterm2  50096