Theorem eldif 2900

Description: Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994.)

Assertion

Ref	Expression
eldif	⊢ (A ∈ (B ∖ 𝐶) ↔ (A ∈ B ∧ ¬ A ∈ 𝐶))

Proof of Theorem eldif

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 2539	. 2 ⊢ (A ∈ (B ∖ 𝐶) → A ∈ V)
2		elex 2539	. . 3 ⊢ (A ∈ B → A ∈ V)
3	2	adantr 261	. 2 ⊢ ((A ∈ B ∧ ¬ A ∈ 𝐶) → A ∈ V)
4		eleq1 2078	. . . 4 ⊢ (x = A → (x ∈ B ↔ A ∈ B))
5		eleq1 2078	. . . . 5 ⊢ (x = A → (x ∈ 𝐶 ↔ A ∈ 𝐶))
6	5	notbid 579	. . . 4 ⊢ (x = A → (¬ x ∈ 𝐶 ↔ ¬ A ∈ 𝐶))
7	4, 6	anbi12d 445	. . 3 ⊢ (x = A → ((x ∈ B ∧ ¬ x ∈ 𝐶) ↔ (A ∈ B ∧ ¬ A ∈ 𝐶)))
8		df-dif 2893	. . 3 ⊢ (B ∖ 𝐶) = {x ∣ (x ∈ B ∧ ¬ x ∈ 𝐶)}
9	7, 8	elab2g 2662	. 2 ⊢ (A ∈ V → (A ∈ (B ∖ 𝐶) ↔ (A ∈ B ∧ ¬ A ∈ 𝐶)))
10	1, 3, 9	pm5.21nii 607	1 ⊢ (A ∈ (B ∖ 𝐶) ↔ (A ∈ B ∧ ¬ A ∈ 𝐶))

Syntax hints:  ¬ wn 3   ∧ wa 97   ↔ wb 98   = wceq 1226   ∈ wcel 1370  Vcvv 2531   ∖ cdif 2887

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 532  ax-in2 533  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000

This theorem depends on definitions:  df-bi 110  df-tru 1229  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-v 2533  df-dif 2893

This theorem is referenced by:  eldifd  2901  eldifad  2902  eldifbd  2903  difeqri  3037  eldifi  3039  eldifn  3040  difdif  3042  ssconb  3049  sscon  3050  ssdif  3051  raldifb  3056  ssddif  3144  unssdif  3145  inssdif  3146  difin  3147  unssin  3149  inssun  3150  invdif  3152  indif  3153  difundi  3162  difindiss  3164  indifdir  3166  undif3ss  3171  difin2  3172  symdifxor  3176  dfnul2  3199  reldisj  3244  disj3  3245  undif4  3257  ssdif0im  3259  inssdif0im  3264  ssundifim  3279  eldifsn  3465  difprsnss  3472  iundif2ss  3692  iindif2m  3694  brdif  3782  unidif0  3890  eldifpw  4154  elirr  4204  en2lp  4212  difopab  4392  intirr  4634  cnvdif  4653  imadiflem  4900  imadif  4901  xrlenlt  6679