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.

Step	Hyp	Ref	Expression
1		elex 2763	. 2 |- ( A e. ( B \ C ) -> A e. _V )
2		elex 2763	. . 3 |- ( A e. B -> A e. _V )
3	2	adantr 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 ) )
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 3146	. . 3 |- ( B \ C ) = { x | ( x e. B /\ -. x e. C ) }
9	7, 8	elab2g 2899	. 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 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