Theorem elind 4100

Description: Deduce membership in an intersection of two classes. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
elind.1	⊢ (𝜑 → 𝑋 ∈ 𝐴)
elind.2	⊢ (𝜑 → 𝑋 ∈ 𝐵)

Assertion

Ref	Expression
elind	⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))

Proof of Theorem elind

Step	Hyp	Ref	Expression
1		elind.1	. 2 ⊢ (𝜑 → 𝑋 ∈ 𝐴)
2		elind.2	. 2 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
3		elin 4096	. 2 ⊢ (𝑋 ∈ (𝐴 ∩ 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵))
4	1, 2, 3	sylanbrc 595	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:  fvelima2  6968  fvelimad  6983  fnfvimad  7271  fnwe2lem3  8184  tfrlem5  8425  uniinqs  8856  unifpw  9382  f1opwfi  9383  fissuni  9384  fipreima  9385  elfir  9444  inelfi  9447  cantnfcl  9705  frrlem15  9798  tskwe  10068  infpwfidom  10146  infpwfien  10180  ackbij2lem1  10335  ackbij1lem3  10338  ackbij1lem4  10339  ackbij1lem6  10341  ackbij1lem11  10346  fin23lem24  10439  isfin1-3  10503  fpwwe2lem11  10765  fpwwe  10770  canthnumlem  10772  fz1isolem  14647  ccatf1  14777  isprm7  16928  setsstruct2  17396  strfv2d  17423  submre  17825  submrc  17852  isacs2  17877  coffth  18163  catcoppccl  18342  catcfuccl  18343  catcxpccl  18431  isdrs2  18530  fpwipodrs  18764  insubm  19064  sylow2a  19884  lsmmod  19940  lsmdisj  19946  lsmdisj2  19947  subgdisj1  19956  frgpnabllem1  20138  dmdprdd  20266  dprdfeq0  20289  dprdres  20295  dprddisj2  20306  dprd2da  20309  dmdprdsplit2lem  20312  ablfacrp  20333  pgpfac1lem3a  20343  pgpfac1lem3  20344  pgpfaclem1  20348  zrinitorngc  20945  zrtermorngc  20946  zrzeroorngc  20947  zrtermoringc  20978  zrninitoringc  20979  cntzsdrg  21110  2idl0  21605  2idl1  21606  ssdifidlprm  21693  zringlpirlem1  21823  zringlpirlem3  21825  irinitoringc  21840  nzerooringczr  21841  aspval  22235  mplind  22434  pmatcoe1fsupp  23074  baspartn  23327  bastg  23339  clsval2  23423  isopn3  23439  restbas  23531  lmss  23671  cmpcovf  23764  discmp  23771  cmpsublem  23772  cmpsub  23773  isconn2  23787  connclo  23788  llynlly  23851  restnlly  23856  restlly  23857  islly2  23858  llyrest  23859  nllyrest  23860  llyidm  23862  nllyidm  23863  hausllycmp  23868  cldllycmp  23869  lly1stc  23870  dislly  23871  llycmpkgen2  23924  1stckgenlem  23927  txlly  24010  txnlly  24011  txtube  24014  txcmplem1  24015  txcmplem2  24016  xkococnlem  24033  basqtop  24085  tgqtop  24086  infil  24237  fmfnfmlem4  24331  hauspwpwf1  24361  tgpconncompss  24488  ustfilxp  24587  metrest  24898  tgioo  25170  zdis  25191  icccmplem1  25197  icccmplem2  25198  reconnlem2  25202  xrge0tsms  25209  cnheibor  25331  cnllycmp  25332  ncvs1  25533  cphsqrtcl  25560  cmetcaulem  25664  ovollb2lem  25864  ovolctb  25866  ovolshftlem1  25885  ovolscalem1  25889  ovolicc1  25892  ioombl1lem1  25934  ioorf  25949  ioorcl  25953  dyadf  25967  vitalilem2  25985  vitali  25989  i1faddlem  26069  i1fmullem  26070  dvres2lem  26285  dvaddbr  26313  dvmulbr  26314  lhop1lem  26388  lhop  26391  dvcnvrelem2  26393  ig1peu  26548  tayl0  26746  rlimcnp2  27351  xrlimcnp  27353  ppisval  27488  ppisval2  27489  ppinprm  27536  chtnprm  27538  2sqlem7  27808  chebbnd1lem1  27853  tglnpt4  29180  footexALT  29250  footexlem2  29252  foot  29254  footne  29255  perprag  29259  colperpexlem3  29265  mideulem2  29267  lnoppinn0  29288  lnopp2hpgb  29298  colopp  29304  lnincplng  29319  plngrotlem1  29322  plngrotlem2  29323  lnssplng  29327  lmieu  29346  lmimid  29356  hypcgrlem1  29362  hypcgrlem2  29363  trgcopyeulem  29369  tgaaddcpbllem1  29406  tgaaddcpbl  29409  angmgmaddeu2  29437  angmgmaddeu3  29438  angmgmaddov2lem  29444  angmgmaddcpbl  29447  angmgmaddrid  29450  dfprlng2  29482  prlngmolem1  29487  prlngmolem2  29488  prlngmo2  29491  prlngpln4  29493  prlngmid2  29496  prlngsymquadlem  29498  quadcgrprlng  29501  f1otrg  29505  eengtrkg  29621  shuni  31959  5oalem1  32313  5oalem2  32314  5oalem4  32316  5oalem5  32317  3oalem2  32322  pjclem4  32858  pj3si  32866  xrge0tsmsd  33733  wrdpmtrlast  33753  edompid  33961  idlinsubrg  34085  qsdrngilem  34122  qsdrngi  34123  pidufd  34179  rngunsnply1chr2lem2  34251  exsslsb  34340  lindsunlem  34367  lbsdiflsp0  34369  dimkerim  34370  irngss  34430  cmpcref  34593  cmppcmp  34601  dispcmp  34602  zarcmplem  34624  prsdm  34657  prsrn  34658  pnfneige0  34694  qqhucn  34735  rrhqima  34757  gsumesum  34802  esumcst  34806  esum2d  34836  sigainb  34880  inelpisys  34898  dynkin  34911  eulerpartlemgh  35121  eulerpartlemgs2  35123  eulerpartlemn  35124  sseqmw  35134  sseqf  35135  sseqp1  35138  fibp1  35144  bnj1379  35571  bnj1177  35747  cnllysconn  36218  rellysconn  36224  cvmsss2  36247  cvmcov2  36248  cvmopnlem  36251  mclsind  36543  weiunfr  37470  poimirlem30  38836  blbnd  38987  ssbnd  38988  heiborlem1  39011  heiborlem8  39018  heibor  39021  mndomgmid  39071  pmodlem1  41169  pclfinN  41223  mapdunirnN  42973  hdmaprnlem9N  43180  mhpind  43888  elrfi  43971  elrfirn  43972  dfac11  44330  kelac1  44331  kelac2lem  44332  dfac21  44334  islssfgi  44340  filnm  44358  lpirlnr  44384  hbtlem6  44396  hbt  44397  iocinico  44475  ishfstruct  46295  restuni3  46406  disjinfi  46480  iooabslt  46784  iocopn  46805  icoopn  46810  uzinico  46844  limciccioolb  46906  limcicciooub  46920  islpcn  46922  limcresioolb  46926  limcleqr  46927  limsuppnfdlem  46984  limsupresxr  47049  liminfresxr  47050  liminfvalxr  47066  liminflelimsupuz  47068  cnrefiisplem  47112  ioccncflimc  47168  icccncfext  47170  icocncflimc  47172  cncfiooicclem1  47176  itgiccshift  47263  itgperiod  47264  itgsbtaddcnst  47265  stoweidlem57  47340  fourierdlem20  47410  fourierdlem32  47422  fourierdlem33  47423  fourierdlem48  47437  fourierdlem49  47438  fourierdlem62  47451  fourierdlem71  47460  fouriersw  47514  qndenserrnbllem  47577  qndenserrn  47582  salgencntex  47626  fsumlesge0  47660  sge0tsms  47663  sge0cl  47664  sge0f1o  47665  sge0sup  47674  sge0resplit  47689  sge0iunmptlemre  47698  sge0fodjrnlem  47699  sge0rpcpnf  47704  sge0xaddlem1  47716  ovolval4lem2  47933  sssmf  48021  smflimlem3  48056  smfsuplem1  48094  fcores  48410  prproropf1olem2  48859  iinfconstbaslem  50510  ffthoppf  50612  uobeqw  50666  uobeq  50667  swapfiso  50738  swapciso  50739  fucoppcffth  50877  thincciso  50919  thinccisod  50920  termcterm  50979  termcterm2  50980  termcterm3  50981  termcciso  50982  termc2  50984  diagciso  51008  diagcic  51009  uobeqterm  51015