NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  elin GIF version

Theorem elin 3219
Description: Membership in intersection. (Contributed by SF, 10-Jan-2015.)
Assertion
Ref Expression
elin (A (BC) ↔ (A B A C))

Proof of Theorem elin
StepHypRef Expression
1 elex 2867 . 2 (A (BC) → A V)
2 elex 2867 . . 3 (A BA V)
32adantr 451 . 2 ((A B A C) → A V)
4 elcomplg 3218 . . . 4 (A V → (A ∼ (BC) ↔ ¬ A (BC)))
5 elning 3217 . . . . 5 (A V → (A (BC) ↔ (A B A C)))
65notbid 285 . . . 4 (A V → (¬ A (BC) ↔ ¬ (A B A C)))
74, 6bitrd 244 . . 3 (A V → (A ∼ (BC) ↔ ¬ (A B A C)))
8 df-in 3213 . . . 4 (BC) = ∼ (BC)
98eleq2i 2417 . . 3 (A (BC) ↔ A ∼ (BC))
10 df-nan 1288 . . . 4 ((A B A C) ↔ ¬ (A B A C))
1110con2bii 322 . . 3 ((A B A C) ↔ ¬ (A B A C))
127, 9, 113bitr4g 279 . 2 (A V → (A (BC) ↔ (A B A C)))
131, 3, 12pm5.21nii 342 1 (A (BC) ↔ (A B A C))
Colors of variables: wff setvar class
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  6243  nmembers1lem1  6267  nncdiv3lem1  6273  nncdiv3lem2  6274  spacvallem1  6279  nchoicelem11  6297  nchoicelem18  6304  fnfreclem1  6315
  Copyright terms: Public domain W3C validator