Theorem elin 3219

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

Assertion

Ref	Expression
elin	⊢ (A ∈ (B ∩ C) ↔ (A ∈ B ∧ A ∈ C))

Proof of Theorem elin

Step	Hyp	Ref	Expression
1		elex 2867	. 2 ⊢ (A ∈ (B ∩ C) → A ∈ V)
2		elex 2867	. . 3 ⊢ (A ∈ B → A ∈ V)
3	2	adantr 451	. 2 ⊢ ((A ∈ B ∧ A ∈ C) → A ∈ V)
4		elcomplg 3218	. . . 4 ⊢ (A ∈ V → (A ∈ ∼ (B ⩃ C) ↔ ¬ A ∈ (B ⩃ C)))
5		elning 3217	. . . . 5 ⊢ (A ∈ V → (A ∈ (B ⩃ C) ↔ (A ∈ B ⊼ A ∈ C)))
6	5	notbid 285	. . . 4 ⊢ (A ∈ V → (¬ A ∈ (B ⩃ C) ↔ ¬ (A ∈ B ⊼ A ∈ C)))
7	4, 6	bitrd 244	. . 3 ⊢ (A ∈ V → (A ∈ ∼ (B ⩃ C) ↔ ¬ (A ∈ B ⊼ A ∈ C)))
8		df-in 3213	. . . 4 ⊢ (B ∩ C) = ∼ (B ⩃ C)
9	8	eleq2i 2417	. . 3 ⊢ (A ∈ (B ∩ C) ↔ A ∈ ∼ (B ⩃ C))
10		df-nan 1288	. . . 4 ⊢ ((A ∈ B ⊼ A ∈ C) ↔ ¬ (A ∈ B ∧ A ∈ C))
11	10	con2bii 322	. . 3 ⊢ ((A ∈ B ∧ A ∈ C) ↔ ¬ (A ∈ B ⊼ A ∈ C))
12	7, 9, 11	3bitr4g 279	. 2 ⊢ (A ∈ V → (A ∈ (B ∩ C) ↔ (A ∈ B ∧ A ∈ C)))
13	1, 3, 12	pm5.21nii 342	1 ⊢ (A ∈ (B ∩ C) ↔ (A ∈ B ∧ A ∈ C))

Syntax hints:  ¬ wn 3   ↔ wb 176   ∧ wa 358   ⊼ wnan 1287   ∈ wcel 1710  Vcvv 2859   ⩃ cnin 3204   ∼ ccompl 3205   ∩ cin 3208

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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 2478  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213

This theorem is referenced by:  eldif  3221  dfss2  3262  elin2  3446  elin3  3447  incom  3448  ineqri  3449  ineq1  3450  rabbi2dva  3463  inass  3465  inss1  3475  ssin  3477  ssrin  3480  dfss4  3489  difin  3492  indi  3501  undi  3502  unineq  3505  indifdir  3511  difin2  3516  inrab2  3528  disj  3591  inelcm  3605  difin0ss  3616  inssdif0  3617  inundif  3628  uniin  3911  intun  3958  intpr  3959  elrint  3967  iunin2  4030  iinin2  4036  elriin  4038  iinxprg  4043  elpw1  4144  pw1in  4164  eluni1g  4172  opkelcokg  4261  inxpk  4277  cnvkexg  4286  ssetkex  4294  sikexg  4296  dfimak2  4298  ins2kexg  4305  ins3kexg  4306  dfidk2  4313  ndisjrelk  4323  peano5  4409  nnsucelrlem1  4424  nndisjeq  4429  nnceleq  4430  preaddccan2lem1  4454  ltfinex  4464  ssfin  4470  ncfinraiselem2  4480  ncfinlowerlem1  4482  eqtfinrelk  4486  evenfinex  4503  oddfinex  4504  evenodddisjlem1  4515  nnadjoinlem1  4519  nnadjoin  4520  nnpweqlem1  4522  srelk  4524  sfintfinlem1  4531  tfinnnlem1  4533  sfinltfin  4535  spfinex  4537  spfininduct  4540  vinf  4555  dfphi2  4569  brin  4693  setconslem2  4732  setconslem4  4734  setconslem6  4736  dfswap2  4741  inopab  4862  inxp  4863  dmin  4913  dminss  5041  imainss  5042  ssrnres  5059  cnvresima  5077  dfco2a  5081  dfxp2  5113  2elresin  5194  nfvres  5352  inpreima  5409  respreima  5410  funfvima  5459  isomin  5496  isoini  5497  dmtxp  5802  releqmpt  5808  composeex  5820  addcfnex  5824  funsex  5828  fnsex  5832  crossex  5850  domfnex  5870  ranfnex  5871  clos1ex  5876  clos1induct  5880  transex  5910  refex  5911  antisymex  5912  connexex  5913  foundex  5914  extex  5915  symex  5916  mapexi  6003  fnpm  6008  mapval2  6018  nenpw1pwlem1  6084  ovmuc  6130  mucex  6133  nceleq  6149  ovcelem1  6171  ceex  6174  tcfnex  6244  nmembers1lem1  6268  nncdiv3lem1  6275  nncdiv3lem2  6276  spacvallem1  6281  nchoicelem11  6299  nchoicelem18  6306  fnfreclem1  6317