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

Theorem inexg 4100
Description: The intersection of two sets is a set. (Contributed by SF, 12-Jan-2015.)
Assertion
Ref Expression
inexg ((A V B W) → (AB) V)

Proof of Theorem inexg
StepHypRef Expression
1 df-in 3213 . 2 (AB) = ∼ (AB)
2 ninexg 4097 . . 3 ((A V B W) → (AB) V)
3 complexg 4099 . . 3 ((AB) V → ∼ (AB) V)
42, 3syl 15 . 2 ((A V B W) → ∼ (AB) V)
51, 4syl5eqel 2437 1 ((A V B W) → (AB) V)
Colors of variables: wff setvar class
Syntax hints:  wi 4   wa 358   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  ax-nin 4078
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:  difexg  4102  inex  4105  xpkexg  4288  imakexg  4299  cokexg  4309  peano5  4409  spfininduct  4540  xpexg  5114  resexg  5116  txpexg  5784  fixexg  5788  clos1induct  5880  frds  5935  pmex  6005  nenpw1pwlem1  6084  ovcelem1  6171  fnfreclem1  6316
  Copyright terms: Public domain W3C validator