Theorem eldif 3163

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 3156	. . 3 |- ( B \ C ) = { x | ( x e. B /\ -. x e. C ) }
9	7, 8	elab2g 2908	. 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 3151

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 3156

This theorem is referenced by:  eldifd  3164  eldifad  3165  eldifbd  3166  difeqri  3280  eldifi  3282  eldifn  3283  difdif  3285  ddifstab  3292  ssconb  3293  sscon  3294  ssdif  3295  raldifb  3300  dfss4st  3393  ssddif  3394  unssdif  3395  inssdif  3396  difin  3397  unssin  3399  inssun  3400  invdif  3402  indif  3403  difundi  3412  difindiss  3414  indifdir  3416  undif3ss  3421  difin2  3422  symdifxor  3426  dfnul2  3449  reldisj  3499  disj3  3500  undif4  3510  ssdif0im  3512  inssdif0im  3515  ssundifim  3531  eldifpr  3646  eldiftp  3665  eldifsn  3746  difprsnss  3757  iundif2ss  3979  iindif2m  3981  brdif  4083  unidif0  4197  eldifpw  4509  elirr  4574  en2lp  4587  difopab  4796  intirr  5053  cnvdif  5073  imadiflem  5334  imadif  5335  elfi2  7033  xrlenlt  8086  nzadd  9372  irradd  9714  irrmul  9715  fzdifsuc  10150  fisumss  11538  prodssdc  11735  fprodssdc  11736  inffinp1  12589  bj-charfunr  15372