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

Theorem eldif 3153
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 2763 . 2  |-  ( A  e.  ( B  \  C )  ->  A  e.  _V )
2 elex 2763 . . 3  |-  ( A  e.  B  ->  A  e.  _V )
32adantr 276 . 2  |-  ( ( A  e.  B  /\  -.  A  e.  C
)  ->  A  e.  _V )
4 eleq1 2252 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
5 eleq1 2252 . . . . 5  |-  ( x  =  A  ->  (
x  e.  C  <->  A  e.  C ) )
65notbid 668 . . . 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 3146 . . 3  |-  ( B 
\  C )  =  { x  |  ( x  e.  B  /\  -.  x  e.  C
) }
97, 8elab2g 2899 . 2  |-  ( A  e.  _V  ->  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) ) )
101, 3, 9pm5.21nii 705 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 1364    e. wcel 2160   _Vcvv 2752    \ cdif 3141
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 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171
This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-dif 3146
This theorem is referenced by:  eldifd  3154  eldifad  3155  eldifbd  3156  difeqri  3270  eldifi  3272  eldifn  3273  difdif  3275  ddifstab  3282  ssconb  3283  sscon  3284  ssdif  3285  raldifb  3290  dfss4st  3383  ssddif  3384  unssdif  3385  inssdif  3386  difin  3387  unssin  3389  inssun  3390  invdif  3392  indif  3393  difundi  3402  difindiss  3404  indifdir  3406  undif3ss  3411  difin2  3412  symdifxor  3416  dfnul2  3439  reldisj  3489  disj3  3490  undif4  3500  ssdif0im  3502  inssdif0im  3505  ssundifim  3521  eldifpr  3634  eldiftp  3653  eldifsn  3734  difprsnss  3745  iundif2ss  3967  iindif2m  3969  brdif  4071  unidif0  4185  eldifpw  4495  elirr  4558  en2lp  4571  difopab  4778  intirr  5033  cnvdif  5053  imadiflem  5314  imadif  5315  elfi2  7001  xrlenlt  8052  nzadd  9335  irradd  9676  irrmul  9677  fzdifsuc  10111  fisumss  11432  prodssdc  11629  fprodssdc  11630  inffinp1  12480  bj-charfunr  15020
  Copyright terms: Public domain W3C validator