Theorem elind 4175

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 3942	. 2 ⊢ (𝑋 ∈ (𝐴 ∩ 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵))
4	1, 2, 3	sylanbrc 583	1 ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-in 3933

This theorem is referenced by:  fvelima2  6930  fvelimad  6945  fnfvimad  7225  tfrlem5  8392  uniinqs  8809  unifpw  9365  f1opwfi  9366  fissuni  9367  fipreima  9368  elfir  9425  inelfi  9428  cantnfcl  9679  frrlem15  9769  tskwe  9962  infpwfidom  10040  infpwfien  10074  ackbij2lem1  10230  ackbij1lem3  10233  ackbij1lem4  10234  ackbij1lem6  10236  ackbij1lem11  10241  fin23lem24  10334  isfin1-3  10398  fpwwe2lem11  10653  fpwwe  10658  canthnumlem  10660  fz1isolem  14477  isprm7  16725  setsstruct2  17191  strfv2d  17218  submre  17615  submrc  17638  isacs2  17663  coffth  17949  catcoppccl  18128  catcfuccl  18129  catcxpccl  18217  isdrs2  18316  fpwipodrs  18548  insubm  18794  sylow2a  19598  lsmmod  19654  lsmdisj  19660  lsmdisj2  19661  subgdisj1  19670  frgpnabllem1  19852  dmdprdd  19980  dprdfeq0  20003  dprdres  20009  dprddisj2  20020  dprd2da  20023  dmdprdsplit2lem  20026  ablfacrp  20047  pgpfac1lem3a  20057  pgpfac1lem3  20058  pgpfaclem1  20062  zrinitorngc  20600  zrtermorngc  20601  zrzeroorngc  20602  zrtermoringc  20633  zrninitoringc  20634  cntzsdrg  20760  2idl0  21219  2idl1  21220  zringlpirlem1  21421  zringlpirlem3  21423  irinitoringc  21438  nzerooringczr  21439  aspval  21831  mplind  22026  pmatcoe1fsupp  22637  baspartn  22890  bastg  22902  clsval2  22986  isopn3  23002  restbas  23094  lmss  23234  cmpcovf  23327  discmp  23334  cmpsublem  23335  cmpsub  23336  isconn2  23350  connclo  23351  llynlly  23413  restnlly  23418  restlly  23419  islly2  23420  llyrest  23421  nllyrest  23422  llyidm  23424  nllyidm  23425  hausllycmp  23430  cldllycmp  23431  lly1stc  23432  dislly  23433  llycmpkgen2  23486  1stckgenlem  23489  txlly  23572  txnlly  23573  txtube  23576  txcmplem1  23577  txcmplem2  23578  xkococnlem  23595  basqtop  23647  tgqtop  23648  infil  23799  fmfnfmlem4  23893  hauspwpwf1  23923  tgpconncompss  24050  ustfilxp  24149  metrest  24461  tgioo  24733  zdis  24754  icccmplem1  24760  icccmplem2  24761  reconnlem2  24765  xrge0tsms  24772  cnheibor  24903  cnllycmp  24904  ncvs1  25107  cphsqrtcl  25134  cmetcaulem  25238  ovollb2lem  25439  ovolctb  25441  ovolshftlem1  25460  ovolscalem1  25464  ovolicc1  25467  ioombl1lem1  25509  ioorf  25524  ioorcl  25528  dyadf  25542  vitalilem2  25560  vitali  25564  i1faddlem  25644  i1fmullem  25645  dvres2lem  25861  dvaddbr  25890  dvmulbr  25891  dvmulbrOLD  25892  lhop1lem  25968  lhop  25971  dvcnvrelem2  25973  ig1peu  26130  tayl0  26319  rlimcnp2  26926  xrlimcnp  26928  ppisval  27064  ppisval2  27065  ppinprm  27112  chtnprm  27114  2sqlem7  27385  chebbnd1lem1  27430  footexALT  28643  footexlem2  28645  foot  28647  footne  28648  perprag  28651  colperpexlem3  28657  mideulem2  28659  lnopp2hpgb  28688  colopp  28694  lmieu  28709  lmimid  28719  hypcgrlem1  28724  hypcgrlem2  28725  trgcopyeulem  28730  f1otrg  28796  eengtrkg  28911  shuni  31227  5oalem1  31581  5oalem2  31582  5oalem4  31584  5oalem5  31585  3oalem2  31590  pjclem4  32126  pj3si  32134  ccatf1  32870  xrge0tsmsd  33002  wrdpmtrlast  33050  idlinsubrg  33392  ssdifidlprm  33419  qsdrngilem  33455  qsdrngi  33456  pidufd  33504  exsslsb  33582  lindsunlem  33610  lbsdiflsp0  33612  dimkerim  33613  irngss  33674  cmpcref  33827  cmppcmp  33835  dispcmp  33836  zarcmplem  33858  prsdm  33891  prsrn  33892  pnfneige0  33928  qqhucn  33969  rrhqima  33991  gsumesum  34036  esumcst  34040  esum2d  34070  sigainb  34113  inelpisys  34131  dynkin  34144  eulerpartlemgh  34356  eulerpartlemgs2  34358  eulerpartlemn  34359  sseqmw  34369  sseqf  34370  sseqp1  34373  fibp1  34379  bnj1379  34807  bnj1177  34983  cnllysconn  35213  rellysconn  35219  cvmsss2  35242  cvmcov2  35243  cvmopnlem  35246  mclsind  35538  weiunfr  36431  poimirlem30  37620  blbnd  37757  ssbnd  37758  heiborlem1  37781  heiborlem8  37788  heibor  37791  mndomgmid  37841  pmodlem1  39811  pclfinN  39865  mapdunirnN  41615  hdmaprnlem9N  41822  mhpind  42564  elrfi  42664  elrfirn  42665  fnwe2lem2  43022  dfac11  43033  kelac1  43034  kelac2lem  43035  dfac21  43037  islssfgi  43043  filnm  43061  lpirlnr  43088  hbtlem6  43100  hbt  43101  iocinico  43183  restuni3  45090  disjinfi  45164  iooabslt  45476  iocopn  45497  icoopn  45502  uzinico  45536  limciccioolb  45598  limcicciooub  45614  islpcn  45616  limcresioolb  45620  limcleqr  45621  limsuppnfdlem  45678  limsupresxr  45743  liminfresxr  45744  liminfvalxr  45760  liminflelimsupuz  45762  cnrefiisplem  45806  ioccncflimc  45862  icccncfext  45864  icocncflimc  45866  cncfiooicclem1  45870  itgiccshift  45957  itgperiod  45958  itgsbtaddcnst  45959  stoweidlem57  46034  fourierdlem20  46104  fourierdlem32  46116  fourierdlem33  46117  fourierdlem48  46131  fourierdlem49  46132  fourierdlem62  46145  fourierdlem71  46154  fouriersw  46208  qndenserrnbllem  46271  qndenserrn  46276  salgencntex  46320  fsumlesge0  46354  sge0tsms  46357  sge0cl  46358  sge0f1o  46359  sge0sup  46368  sge0resplit  46383  sge0iunmptlemre  46392  sge0fodjrnlem  46393  sge0rpcpnf  46398  sge0xaddlem1  46410  ovolval4lem2  46627  sssmf  46715  smflimlem3  46750  smfsuplem1  46788  fcores  47044  prproropf1olem2  47466  iinfconstbaslem  48980  swapfiso  49150  swapciso  49151  thincciso  49287  thinccisod  49288  termcterm  49346  termcterm2  49347  termcterm3  49348  termcciso  49349  termc2  49351  diagciso  49372  diagcic  49373