Theorem elin2d 4105

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ∩ cin 4092

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-in 4094

This theorem is used by:  f1opwfi  9383  elfiun  9459  ordtypelem3  9551  infpwfien  10180  ttukeylem6  10631  fpwwe2lem11  10765  explecnv  16078  bitsinv1  16656  smuval2  16696  firest  17653  sscres  18048  funcres2c  18128  coffth  18163  rescfth  18164  catcoppccl  18342  catcfuccl  18343  catcxpccl  18431  psssdm2  18805  sylow2a  19884  frgpnabllem2  20139  idomdomd  21028  sralmod  21513  2idlridld  21599  ssdifidlprm  21693  zringlpirlem3  21825  mplind  22434  neiptoptop  23504  restbas  23531  ordtrest  23575  subbascn  23627  lmss  23671  cnconn  23795  clsconn  23803  conncompclo  23808  subislly  23855  cldllycmp  23869  1stckgenlem  23927  txcls  23978  txcnp  23994  txtube  24014  txcmplem1  24015  txkgen  24026  xkopt  24029  xkococnlem  24033  txconn  24063  basqtop  24085  tgqtop  24086  kqnrmlem1  24117  kqnrmlem2  24118  nrmhmph  24168  uzrest  24271  alexsubALTlem3  24423  ptcmplem2  24427  tsmslem1  24503  tsmsxplem1  24527  tsmsxplem2  24528  tsmsxp  24529  blin2  24803  met2ndci  24896  zdis  25191  reconnlem2  25202  reconn  25203  xrge0gsumle  25208  cnheibor  25331  lebnum  25340  nmoleub2lem3  25491  nmoleub3  25495  caussi  25673  minveclem4b  25807  minveclem4  25808  ovolfcl  25842  ovolfioo  25843  ovolficc  25844  ovolficcss  25845  ovolfsval  25846  ovoliunlem1  25878  ovolicc2lem4  25896  ovolicc2lem5  25897  uniiccdif  25954  uniioovol  25955  uniiccvol  25956  uniioombllem2a  25958  uniioombllem3a  25960  uniioombllem4  25962  uniioombllem5  25963  uniioombllem6  25964  vitalilem2  25985  vitalilem4  25987  ig1peu  26548  taylfvallem1  26741  tayl0  26746  ppisval  27488  chtf  27492  efchtcl  27495  chtge0  27496  ppinprm  27536  chtprm  27537  chtnprm  27538  chtwordi  27540  chtdif  27542  efchtdvds  27543  chtlepsi  27590  chtleppi  27594  pclogsum  27599  chpval2  27602  chpchtsum  27603  chpub  27604  chebbnd1lem1  27853  chtppilimlem1  27857  rplogsumlem2  27869  tglnpt4  29180  perpneq  29246  ragperp  29249  lnincplng  29319  angmgmaddeu1  29436  perpprlng  29485  prlngplngtr  29494  quadcgrprlng  29501  tocyc01  33778  cyc3evpm  33810  cycpmconjslem2  33815  cyc3conja  33817  mxidlirred  34101  dflringlem3  34132  dflring4  34134  pidufd  34179  1arithufdlem4  34183  ressdeg1  34201  rngunsnply1chr2lem2  34251  exsslsb  34340  lbsdiflsp0  34369  irngss  34430  rtelextdg2lem  34469  cmpcref  34593  esum2d  34836  ispisys2  34897  sigapisys  34899  sigapildsyslem  34905  sigapildsys  34906  sseqf  35135  tgoldbachgt  35403  bnj1172  35742  weiunfrlem  37467  dfttc4  37533  mhpind  43888  ismnushort  45546  cnrefiisplem  47112  hoiqssbllem3  47907  sssmf  48021  smflimlem3  48056  tmachlem-finscan  48218  tmachlem-exagreecover  48229  iinfconstbas  50511  ffthoppf  50612  fucoppc  50876  termcterm  50979  termcterm2  50980