Theorem elin 3220

Description: Membership in intersection. (Contributed by SF, 10-Jan-2015.)

Assertion

Ref	Expression
elin	|- (A e. (B i^i C) <-> (A e. B /\ A e. C))

Proof of Theorem elin

Step	Hyp	Ref	Expression
1		elex 2868	. 2 |- (A e. (B i^i C) -> A e. _V)
2		elex 2868	. . 3 |- (A e. B -> A e. _V)
3	2	adantr 451	. 2 |- ((A e. B /\ A e. C) -> A e. _V)
4		elcomplg 3219	. . . 4 |- (A e. _V -> (A e. ∼ (B &ncap C) <-> -. A e. (B &ncap C)))
5		elning 3218	. . . . 5 |- (A e. _V -> (A e. (B &ncap C) <-> (A e. B -/\ A e. C)))
6	5	notbid 285	. . . 4 |- (A e. _V -> (-. A e. (B &ncap C) <-> -. (A e. B -/\ A e. C)))
7	4, 6	bitrd 244	. . 3 |- (A e. _V -> (A e. ∼ (B &ncap C) <-> -. (A e. B -/\ A e. C)))
8		df-in 3214	. . . 4 |- (B i^i C) = ∼ (B &ncap C)
9	8	eleq2i 2417	. . 3 |- (A e. (B i^i C) <-> A e. ∼ (B &ncap C))
10		df-nan 1288	. . . 4 |- ((A e. B -/\ A e. C) <-> -. (A e. B /\ A e. C))
11	10	con2bii 322	. . 3 |- ((A e. B /\ A e. C) <-> -. (A e. B -/\ A e. C))
12	7, 9, 11	3bitr4g 279	. 2 |- (A e. _V -> (A e. (B i^i C) <-> (A e. B /\ A e. C)))
13	1, 3, 12	pm5.21nii 342	1 |- (A e. (B i^i C) <-> (A e. B /\ A e. C))

Syntax hints:  -. wn 3   <-> wb 176   /\ wa 358   -/\ wnan 1287   e. wcel 1710  _Vcvv 2860   &ncap cnin 3205   ∼ ccompl 3206   i^i cin 3209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-v 2862  df-nin 3212  df-compl 3213  df-in 3214

This theorem is referenced by:  eldif  3222  dfss2  3263  elin2  3447  elin3  3448  incom  3449  ineqri  3450  ineq1  3451  rabbi2dva  3464  inass  3466  inss1  3476  ssin  3478  ssrin  3481  dfss4  3490  difin  3493  indi  3502  undi  3503  unineq  3506  indifdir  3512  difin2  3517  inrab2  3529  disj  3592  inelcm  3606  difin0ss  3617  inssdif0  3618  inundif  3629  uniin  3912  intun  3959  intpr  3960  elrint  3968  iunin2  4031  iinin2  4037  elriin  4039  iinxprg  4044  elpw1  4145  pw1in  4165  eluni1g  4173  opkelcokg  4262  inxpk  4278  cnvkexg  4287  ssetkex  4295  sikexg  4297  dfimak2  4299  ins2kexg  4306  ins3kexg  4307  dfidk2  4314  ndisjrelk  4324  peano5  4410  nnsucelrlem1  4425  nndisjeq  4430  nnceleq  4431  preaddccan2lem1  4455  ltfinex  4465  ssfin  4471  ncfinraiselem2  4481  ncfinlowerlem1  4483  eqtfinrelk  4487  evenfinex  4504  oddfinex  4505  evenodddisjlem1  4516  nnadjoinlem1  4520  nnadjoin  4521  nnpweqlem1  4523  srelk  4525  sfintfinlem1  4532  tfinnnlem1  4534  sfinltfin  4536  spfinex  4538  spfininduct  4541  vinf  4556  dfphi2  4570  brin  4694  setconslem2  4733  setconslem4  4735  setconslem6  4737  dfswap2  4742  inopab  4863  inxp  4864  dmin  4914  dminss  5042  imainss  5043  ssrnres  5060  cnvresima  5078  dfco2a  5082  dfxp2  5114  2elresin  5195  nfvres  5353  inpreima  5410  respreima  5411  funfvima  5460  isomin  5497  isoini  5498  dmtxp  5803  releqmpt  5809  composeex  5821  addcfnex  5825  funsex  5829  fnsex  5833  crossex  5851  domfnex  5871  ranfnex  5872  clos1ex  5877  clos1induct  5881  transex  5911  refex  5912  antisymex  5913  connexex  5914  foundex  5915  extex  5916  symex  5917  mapexi  6004  fnpm  6009  mapval2  6019  nenpw1pwlem1  6085  ovmuc  6131  mucex  6134  nceleq  6150  ovcelem1  6172  ceex  6175  tcfnex  6245  nmembers1lem1  6269  nncdiv3lem1  6276  nncdiv3lem2  6277  spacvallem1  6282  nchoicelem11  6300  nchoicelem18  6307  fnfreclem1  6318