Theorem elcompl 3226

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

Hypothesis

Ref	Expression
elbool.1	⊢ A ∈ V

Assertion

Ref	Expression
elcompl	⊢ (A ∈ ∼ B ↔ ¬ A ∈ B)

Proof of Theorem elcompl

Step	Hyp	Ref	Expression
1		elbool.1	. 2 ⊢ A ∈ V
2		elcomplg 3219	. 2 ⊢ (A ∈ V → (A ∈ ∼ B ↔ ¬ A ∈ B))
3	1, 2	ax-mp 5	1 ⊢ (A ∈ ∼ B ↔ ¬ A ∈ B)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 176   ∈ wcel 1710  Vcvv 2860   ∼ ccompl 3206

This proof depends on 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 proof 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

This theorem is used by:  dblcompl  3228  complab  3525  necompl  3545  sscon34  3662  disj5  3891  nincompl  4073  ssofss  4077  dfimak2  4299  dfint3  4319  dfpw2  4328  dfaddc2  4382  elsuc  4414  elsuci  4415  nnsucelrlem1  4425  nnsucelrlem3  4427  nnsucelr  4429  nndisjeq  4430  prepeano4  4452  preaddccan2lem1  4455  ltfinex  4465  ssfin  4471  eqpwrelk  4479  ncfinraiselem2  4481  ncfinraise  4482  ncfinlowerlem1  4483  ncfinlower  4484  eqtfinrelk  4487  tfinsuc  4499  evenfinex  4504  oddfinex  4505  evenodddisjlem1  4516  nnadjoinlem1  4520  nnadjoin  4521  nnpweqlem1  4523  srelk  4525  sfindbl  4531  sfintfinlem1  4532  tfinnnlem1  4534  tfinnn  4535  spfinex  4538  vfin1cltv  4548  nulnnn  4557  dfphi2  4570  dfop2lem1  4574  setconslem2  4733  setconslem3  4734  setconslem7  4738  dfswap2  4742  intirr  5030  brimage  5794  releqel  5808  disjex  5824  epprc  5828  funsex  5829  fnfullfunlem1  5857  fvfullfun  5865  transex  5911  refex  5912  antisymex  5913  connexex  5914  foundex  5915  extex  5916  symex  5917  qsexg  5983  enprmaplem4  6080  nenpw1pwlem1  6085  peano4nc  6151  ovcelem1  6172  ce0nn  6181  el2c  6192  tcfnex  6245  nclennlem1  6249  nnc3n3p1  6279  nchoicelem10  6299  nchoicelem11  6300  nchoicelem16  6305  nchoicelem18  6307  fnfreclem1  6318