Theorem elin2d 4146

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

Syntax hints:   → wi 4   ∈ wcel 2114   ∩ cin 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-in 3897

This theorem is referenced by:  f1opwfi  9259  elfiun  9336  ordtypelem3  9428  infpwfien  9975  ttukeylem6  10427  fpwwe2lem11  10555  explecnv  15821  bitsinv1  16402  smuval2  16442  firest  17386  sscres  17781  funcres2c  17861  coffth  17896  rescfth  17897  catcoppccl  18075  catcfuccl  18076  catcxpccl  18164  psssdm2  18538  sylow2a  19585  frgpnabllem2  19840  idomdomd  20694  sralmod  21174  2idlridld  21245  zringlpirlem3  21454  mplind  22058  neiptoptop  23106  restbas  23133  ordtrest  23177  subbascn  23229  lmss  23273  cnconn  23397  clsconn  23405  conncompclo  23410  subislly  23456  cldllycmp  23470  1stckgenlem  23528  txcls  23579  txcnp  23595  txtube  23615  txcmplem1  23616  txkgen  23627  xkopt  23630  xkococnlem  23634  txconn  23664  basqtop  23686  tgqtop  23687  kqnrmlem1  23718  kqnrmlem2  23719  nrmhmph  23769  uzrest  23872  alexsubALTlem3  24024  ptcmplem2  24028  tsmslem1  24104  tsmsxplem1  24128  tsmsxplem2  24129  tsmsxp  24130  blin2  24404  met2ndci  24497  zdis  24792  reconnlem2  24803  reconn  24804  xrge0gsumle  24809  cnheibor  24932  lebnum  24941  nmoleub2lem3  25092  nmoleub3  25096  caussi  25274  minveclem4b  25408  minveclem4  25409  ovolfcl  25443  ovolfioo  25444  ovolficc  25445  ovolficcss  25446  ovolfsval  25447  ovoliunlem1  25479  ovolicc2lem4  25497  ovolicc2lem5  25498  uniiccdif  25555  uniioovol  25556  uniiccvol  25557  uniioombllem2a  25559  uniioombllem3a  25561  uniioombllem4  25563  uniioombllem5  25564  uniioombllem6  25565  vitalilem2  25586  vitalilem4  25588  ig1peu  26150  taylfvallem1  26333  tayl0  26338  ppisval  27081  chtf  27085  efchtcl  27088  chtge0  27089  ppinprm  27129  chtprm  27130  chtnprm  27131  chtwordi  27133  chtdif  27135  efchtdvds  27136  chtlepsi  27183  chtleppi  27187  pclogsum  27192  chpval2  27195  chpchtsum  27196  chpub  27197  chebbnd1lem1  27446  chtppilimlem1  27450  rplogsumlem2  27462  perpneq  28796  ragperp  28799  tocyc01  33194  cyc3evpm  33226  cycpmconjslem2  33231  cyc3conja  33233  ssdifidlprm  33533  mxidlirred  33547  pidufd  33618  1arithufdlem4  33622  ressdeg1  33641  exsslsb  33756  lbsdiflsp0  33786  irngss  33847  rtelextdg2lem  33886  esum2d  34253  ispisys2  34313  sigapisys  34315  sigapildsyslem  34321  sigapildsys  34322  sseqf  34552  tgoldbachgt  34823  bnj1172  35159  weiunfrlem  36662  dfttc4  36728  mhpind  43041  ismnushort  44746  cnrefiisplem  46275  hoiqssbllem3  47070  smflimlem3  47219  iinfconstbas  49553  ffthoppf  49652  fucoppc  49897  termcterm  50000  termcterm2  50001