Theorem elin2d 4228

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

Syntax hints:   → wi 4   ∈ wcel 2108   ∩ cin 3975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-in 3983

This theorem is referenced by:  f1opwfi  9426  elfiun  9499  ordtypelem3  9589  infpwfien  10131  ttukeylem6  10583  fpwwe2lem11  10710  explecnv  15913  bitsinv1  16488  smuval2  16528  firest  17492  sscres  17884  funcres2c  17968  coffth  18003  rescfth  18004  catcoppccl  18184  catcoppcclOLD  18185  catcfuccl  18186  catcfucclOLD  18187  catcxpccl  18276  catcxpcclOLD  18277  psssdm2  18651  sylow2a  19661  frgpnabllem2  19916  idomdomd  20748  sralmod  21217  2idlridld  21288  zringlpirlem3  21498  mplind  22117  neiptoptop  23160  restbas  23187  ordtrest  23231  subbascn  23283  lmss  23327  cnconn  23451  clsconn  23459  conncompclo  23464  subislly  23510  cldllycmp  23524  1stckgenlem  23582  txcls  23633  txcnp  23649  txtube  23669  txcmplem1  23670  txkgen  23681  xkopt  23684  xkococnlem  23688  txconn  23718  basqtop  23740  tgqtop  23741  kqnrmlem1  23772  kqnrmlem2  23773  nrmhmph  23823  uzrest  23926  alexsubALTlem3  24078  ptcmplem2  24082  tsmslem1  24158  tsmsxplem1  24182  tsmsxplem2  24183  tsmsxp  24184  blin2  24460  met2ndci  24556  zdis  24857  reconnlem2  24868  reconn  24869  xrge0gsumle  24874  cnheibor  25006  lebnum  25015  nmoleub2lem3  25167  nmoleub3  25171  caussi  25350  minveclem4b  25484  minveclem4  25485  ovolfcl  25520  ovolfioo  25521  ovolficc  25522  ovolficcss  25523  ovolfsval  25524  ovoliunlem1  25556  ovolicc2lem4  25574  ovolicc2lem5  25575  uniiccdif  25632  uniioovol  25633  uniiccvol  25634  uniioombllem2a  25636  uniioombllem3a  25638  uniioombllem4  25640  uniioombllem5  25641  uniioombllem6  25642  vitalilem2  25663  vitalilem4  25665  ig1peu  26234  taylfvallem1  26416  tayl0  26421  ppisval  27165  chtf  27169  efchtcl  27172  chtge0  27173  ppinprm  27213  chtprm  27214  chtnprm  27215  chtwordi  27217  chtdif  27219  efchtdvds  27220  chtlepsi  27268  chtleppi  27272  pclogsum  27277  chpval2  27280  chpchtsum  27281  chpub  27282  chebbnd1lem1  27531  chtppilimlem1  27535  rplogsumlem2  27547  perpneq  28740  ragperp  28743  tocyc01  33111  cyc3evpm  33143  cycpmconjslem2  33148  cyc3conja  33150  ssdifidlprm  33451  mxidlirred  33465  pidufd  33536  1arithufdlem4  33540  ressdeg1  33556  lbsdiflsp0  33639  irngss  33687  rtelextdg2lem  33717  esum2d  34057  ispisys2  34117  sigapisys  34119  sigapildsyslem  34125  sigapildsys  34126  sseqf  34357  tgoldbachgt  34640  bnj1172  34977  weiunfrlem  36430  mhpind  42549  ismnushort  44270  cnrefiisplem  45750  hoiqssbllem3  46545  smflimlem3  46694