ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eldif Unicode version

Theorem eldif 3138
Description: Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
Assertion
Ref Expression
eldif  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )

Proof of Theorem eldif
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 elex 2748 . 2  |-  ( A  e.  ( B  \  C )  ->  A  e.  _V )
2 elex 2748 . . 3  |-  ( A  e.  B  ->  A  e.  _V )
32adantr 276 . 2  |-  ( ( A  e.  B  /\  -.  A  e.  C
)  ->  A  e.  _V )
4 eleq1 2240 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
5 eleq1 2240 . . . . 5  |-  ( x  =  A  ->  (
x  e.  C  <->  A  e.  C ) )
65notbid 667 . . . 4  |-  ( x  =  A  ->  ( -.  x  e.  C  <->  -.  A  e.  C ) )
74, 6anbi12d 473 . . 3  |-  ( x  =  A  ->  (
( x  e.  B  /\  -.  x  e.  C
)  <->  ( A  e.  B  /\  -.  A  e.  C ) ) )
8 df-dif 3131 . . 3  |-  ( B 
\  C )  =  { x  |  ( x  e.  B  /\  -.  x  e.  C
) }
97, 8elab2g 2884 . 2  |-  ( A  e.  _V  ->  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) ) )
101, 3, 9pm5.21nii 704 1  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    /\ wa 104    <-> wb 105    = wceq 1353    e. wcel 2148   _Vcvv 2737    \ cdif 3126
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-dif 3131
This theorem is referenced by:  eldifd  3139  eldifad  3140  eldifbd  3141  difeqri  3255  eldifi  3257  eldifn  3258  difdif  3260  ddifstab  3267  ssconb  3268  sscon  3269  ssdif  3270  raldifb  3275  dfss4st  3368  ssddif  3369  unssdif  3370  inssdif  3371  difin  3372  unssin  3374  inssun  3375  invdif  3377  indif  3378  difundi  3387  difindiss  3389  indifdir  3391  undif3ss  3396  difin2  3397  symdifxor  3401  dfnul2  3424  reldisj  3474  disj3  3475  undif4  3485  ssdif0im  3487  inssdif0im  3490  ssundifim  3506  eldifpr  3618  eldiftp  3637  eldifsn  3718  difprsnss  3729  iundif2ss  3949  iindif2m  3951  brdif  4053  unidif0  4164  eldifpw  4473  elirr  4536  en2lp  4549  difopab  4755  intirr  5010  cnvdif  5030  imadiflem  5290  imadif  5291  elfi2  6964  xrlenlt  7999  nzadd  9281  irradd  9622  irrmul  9623  fzdifsuc  10054  fisumss  11371  prodssdc  11568  fprodssdc  11569  inffinp1  12400  bj-charfunr  14184
  Copyright terms: Public domain W3C validator