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

Theorem eldif 3030
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 2652 . 2  |-  ( A  e.  ( B  \  C )  ->  A  e.  _V )
2 elex 2652 . . 3  |-  ( A  e.  B  ->  A  e.  _V )
32adantr 272 . 2  |-  ( ( A  e.  B  /\  -.  A  e.  C
)  ->  A  e.  _V )
4 eleq1 2162 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
5 eleq1 2162 . . . . 5  |-  ( x  =  A  ->  (
x  e.  C  <->  A  e.  C ) )
65notbid 633 . . . 4  |-  ( x  =  A  ->  ( -.  x  e.  C  <->  -.  A  e.  C ) )
74, 6anbi12d 460 . . 3  |-  ( x  =  A  ->  (
( x  e.  B  /\  -.  x  e.  C
)  <->  ( A  e.  B  /\  -.  A  e.  C ) ) )
8 df-dif 3023 . . 3  |-  ( B 
\  C )  =  { x  |  ( x  e.  B  /\  -.  x  e.  C
) }
97, 8elab2g 2784 . 2  |-  ( A  e.  _V  ->  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) ) )
101, 3, 9pm5.21nii 661 1  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    /\ wa 103    <-> wb 104    = wceq 1299    e. wcel 1448   _Vcvv 2641    \ cdif 3018
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 584  ax-in2 585  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082
This theorem depends on definitions:  df-bi 116  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-v 2643  df-dif 3023
This theorem is referenced by:  eldifd  3031  eldifad  3032  eldifbd  3033  difeqri  3143  eldifi  3145  eldifn  3146  difdif  3148  ddifstab  3155  ssconb  3156  sscon  3157  ssdif  3158  raldifb  3163  dfss4st  3256  ssddif  3257  unssdif  3258  inssdif  3259  difin  3260  unssin  3262  inssun  3263  invdif  3265  indif  3266  difundi  3275  difindiss  3277  indifdir  3279  undif3ss  3284  difin2  3285  symdifxor  3289  dfnul2  3312  reldisj  3361  disj3  3362  undif4  3372  ssdif0im  3374  inssdif0im  3377  ssundifim  3393  eldifsn  3597  difprsnss  3605  iundif2ss  3825  iindif2m  3827  brdif  3923  unidif0  4031  eldifpw  4336  elirr  4394  en2lp  4407  difopab  4610  intirr  4861  cnvdif  4881  imadiflem  5138  imadif  5139  xrlenlt  7701  nzadd  8958  irradd  9288  irrmul  9289  fzdifsuc  9702  fisumss  11000  inffinp1  11734
  Copyright terms: Public domain W3C validator