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

Theorem eldif 2955
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 2583 . 2  |-  ( A  e.  ( B  \  C )  ->  A  e.  _V )
2 elex 2583 . . 3  |-  ( A  e.  B  ->  A  e.  _V )
32adantr 265 . 2  |-  ( ( A  e.  B  /\  -.  A  e.  C
)  ->  A  e.  _V )
4 eleq1 2116 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
5 eleq1 2116 . . . . 5  |-  ( x  =  A  ->  (
x  e.  C  <->  A  e.  C ) )
65notbid 602 . . . 4  |-  ( x  =  A  ->  ( -.  x  e.  C  <->  -.  A  e.  C ) )
74, 6anbi12d 450 . . 3  |-  ( x  =  A  ->  (
( x  e.  B  /\  -.  x  e.  C
)  <->  ( A  e.  B  /\  -.  A  e.  C ) ) )
8 df-dif 2948 . . 3  |-  ( B 
\  C )  =  { x  |  ( x  e.  B  /\  -.  x  e.  C
) }
97, 8elab2g 2712 . 2  |-  ( A  e.  _V  ->  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) ) )
101, 3, 9pm5.21nii 630 1  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    /\ wa 101    <-> wb 102    = wceq 1259    e. wcel 1409   _Vcvv 2574    \ cdif 2942
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-v 2576  df-dif 2948
This theorem is referenced by:  eldifd  2956  eldifad  2957  eldifbd  2958  difeqri  3092  eldifi  3094  eldifn  3095  difdif  3097  ssconb  3104  sscon  3105  ssdif  3106  raldifb  3111  ssddif  3199  unssdif  3200  inssdif  3201  difin  3202  unssin  3204  inssun  3205  invdif  3207  indif  3208  difundi  3217  difindiss  3219  indifdir  3221  undif3ss  3226  difin2  3227  symdifxor  3231  dfnul2  3254  reldisj  3299  disj3  3300  undif4  3312  ssdif0im  3314  inssdif0im  3319  ssundifim  3334  eldifsn  3523  difprsnss  3530  iundif2ss  3750  iindif2m  3752  brdif  3840  unidif0  3948  eldifpw  4236  elirr  4294  en2lp  4306  difopab  4497  intirr  4739  cnvdif  4758  imadiflem  5006  imadif  5007  xrlenlt  7143  nzadd  8354  irradd  8678  irrmul  8679  fzdifsuc  9045
  Copyright terms: Public domain W3C validator