Theorem eldif 3139

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 2749	. 2 |- ( A e. ( B \ C ) -> A e. _V )
2		elex 2749	. . 3 |- ( A e. B -> A e. _V )
3	2	adantr 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 ) )
6	5	notbid 667	. . . 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 3132	. . 3 |- ( B \ C ) = { x | ( x e. B /\ -. x e. C ) }
9	7, 8	elab2g 2885	. 2 |- ( A e. _V -> ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) ) )
10	1, 3, 9	pm5.21nii 704	1 |- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )

Syntax hints:   -. wn 3   /\ wa 104   <-> wb 105   = wceq 1353   e. wcel 2148   _Vcvv 2738   \ cdif 3127

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 2740  df-dif 3132

This theorem is referenced by:  eldifd  3140  eldifad  3141  eldifbd  3142  difeqri  3256  eldifi  3258  eldifn  3259  difdif  3261  ddifstab  3268  ssconb  3269  sscon  3270  ssdif  3271  raldifb  3276  dfss4st  3369  ssddif  3370  unssdif  3371  inssdif  3372  difin  3373  unssin  3375  inssun  3376  invdif  3378  indif  3379  difundi  3388  difindiss  3390  indifdir  3392  undif3ss  3397  difin2  3398  symdifxor  3402  dfnul2  3425  reldisj  3475  disj3  3476  undif4  3486  ssdif0im  3488  inssdif0im  3491  ssundifim  3507  eldifpr  3620  eldiftp  3639  eldifsn  3720  difprsnss  3731  iundif2ss  3953  iindif2m  3955  brdif  4057  unidif0  4168  eldifpw  4478  elirr  4541  en2lp  4554  difopab  4761  intirr  5016  cnvdif  5036  imadiflem  5296  imadif  5297  elfi2  6971  xrlenlt  8022  nzadd  9305  irradd  9646  irrmul  9647  fzdifsuc  10081  fisumss  11400  prodssdc  11597  fprodssdc  11598  inffinp1  12430  bj-charfunr  14565