Theorem elin2d 4151

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3906

This theorem is used by:  f1opwfi  9323  elfiun  9400  ordtypelem3  9492  infpwfien  10065  ttukeylem6  10516  fpwwe2lem11  10650  explecnv  15954  bitsinv1  16532  smuval2  16572  firest  17517  sscres  17912  funcres2c  17992  coffth  18027  rescfth  18028  catcoppccl  18206  catcfuccl  18207  catcxpccl  18295  psssdm2  18669  sylow2a  19746  frgpnabllem2  20001  idomdomd  20887  sralmod  21371  2idlridld  21457  ssdifidlprm  21549  zringlpirlem3  21677  mplind  22286  neiptoptop  23356  restbas  23383  ordtrest  23427  subbascn  23479  lmss  23523  cnconn  23647  clsconn  23655  conncompclo  23660  subislly  23707  cldllycmp  23721  1stckgenlem  23779  txcls  23830  txcnp  23846  txtube  23866  txcmplem1  23867  txkgen  23878  xkopt  23881  xkococnlem  23885  txconn  23915  basqtop  23937  tgqtop  23938  kqnrmlem1  23969  kqnrmlem2  23970  nrmhmph  24020  uzrest  24123  alexsubALTlem3  24275  ptcmplem2  24279  tsmslem1  24355  tsmsxplem1  24379  tsmsxplem2  24380  tsmsxp  24381  blin2  24655  met2ndci  24748  zdis  25043  reconnlem2  25054  reconn  25055  xrge0gsumle  25060  cnheibor  25183  lebnum  25192  nmoleub2lem3  25343  nmoleub3  25347  caussi  25525  minveclem4b  25659  minveclem4  25660  ovolfcl  25694  ovolfioo  25695  ovolficc  25696  ovolficcss  25697  ovolfsval  25698  ovoliunlem1  25730  ovolicc2lem4  25748  ovolicc2lem5  25749  uniiccdif  25806  uniioovol  25807  uniiccvol  25808  uniioombllem2a  25810  uniioombllem3a  25812  uniioombllem4  25814  uniioombllem5  25815  uniioombllem6  25816  vitalilem2  25837  vitalilem4  25839  ig1peu  26400  taylfvallem1  26593  tayl0  26598  ppisval  27340  chtf  27344  efchtcl  27347  chtge0  27348  ppinprm  27388  chtprm  27389  chtnprm  27390  chtwordi  27392  chtdif  27394  efchtdvds  27395  chtlepsi  27442  chtleppi  27446  pclogsum  27451  chpval2  27454  chpchtsum  27455  chpub  27456  chebbnd1lem1  27705  chtppilimlem1  27709  rplogsumlem2  27721  tglnpt4  29002  perpneq  29068  ragperp  29071  lnincplng  29141  angmgmaddeu1  29258  perpprlng  29307  prlngplngtr  29316  quadcgrprlng  29323  tocyc01  33558  cyc3evpm  33590  cycpmconjslem2  33595  cyc3conja  33597  mxidlirred  33875  dflringlem3  33906  dflring4  33908  pidufd  33953  1arithufdlem4  33957  ressdeg1  33976  exsslsb  34107  lbsdiflsp0  34136  irngss  34197  rtelextdg2lem  34236  esum2d  34603  ispisys2  34664  sigapisys  34666  sigapildsyslem  34672  sigapildsys  34673  sseqf  34903  tgoldbachgt  35171  bnj1172  35510  weiunfrlem  37083  dfttc4  37149  mhpind  43440  ismnushort  45125  cnrefiisplem  46657  hoiqssbllem3  47452  sssmf  47566  smflimlem3  47601  tmachlem-finscan  47763  tmachlem-exagreecover  47774  iinfconstbas  49992  ffthoppf  50091  fucoppc  50336  termcterm  50439  termcterm2  50440