Theorem eldif 3162

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.

Step	Hyp	Ref	Expression
1		elex 2771	. 2 |- ( A e. ( B \ C ) -> A e. _V )
2		elex 2771	. . 3 |- ( A e. B -> A e. _V )
3	2	adantr 276	. 2 |- ( ( A e. B /\ -. A e. C ) -> A e. _V )
4		eleq1 2256	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2256	. . . . 5 |- ( x = A -> ( x e. C <-> A e. C ) )
6	5	notbid 668	. . . 4 |- ( x = A -> ( -. x e. C <-> -. A e. C ) )
7	4, 6	anbi12d 473	. . 3 |- ( x = A -> ( ( x e. B /\ -. x e. C ) <-> ( A e. B /\ -. A e. C ) ) )
8		df-dif 3155	. . 3 |- ( B \ C ) = { x | ( x e. B /\ -. x e. C ) }
9	7, 8	elab2g 2907	. 2 |- ( A e. _V -> ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) ) )
10	1, 3, 9	pm5.21nii 705	1 |- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )

Syntax hints:   -. wn 3   /\ wa 104   <-> wb 105   = wceq 1364   e. wcel 2164   _Vcvv 2760   \ cdif 3150

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 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-dif 3155

This theorem is referenced by:  eldifd  3163  eldifad  3164  eldifbd  3165  difeqri  3279  eldifi  3281  eldifn  3282  difdif  3284  ddifstab  3291  ssconb  3292  sscon  3293  ssdif  3294  raldifb  3299  dfss4st  3392  ssddif  3393  unssdif  3394  inssdif  3395  difin  3396  unssin  3398  inssun  3399  invdif  3401  indif  3402  difundi  3411  difindiss  3413  indifdir  3415  undif3ss  3420  difin2  3421  symdifxor  3425  dfnul2  3448  reldisj  3498  disj3  3499  undif4  3509  ssdif0im  3511  inssdif0im  3514  ssundifim  3530  eldifpr  3645  eldiftp  3664  eldifsn  3745  difprsnss  3756  iundif2ss  3978  iindif2m  3980  brdif  4082  unidif0  4196  eldifpw  4508  elirr  4573  en2lp  4586  difopab  4795  intirr  5052  cnvdif  5072  imadiflem  5333  imadif  5334  elfi2  7031  xrlenlt  8084  nzadd  9369  irradd  9711  irrmul  9712  fzdifsuc  10147  fisumss  11535  prodssdc  11732  fprodssdc  11733  inffinp1  12586  bj-charfunr  15302