Theorem eldif 3111

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

Assertion

Ref	Expression
eldif	⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))

Proof of Theorem eldif

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 2723	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ V)
2		elex 2723	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 274	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2220	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2220	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	5	notbid 657	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ 𝐶 ↔ ¬ 𝐴 ∈ 𝐶))
7	4, 6	anbi12d 465	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
8		df-dif 3104	. . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 2859	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
10	1, 3, 9	pm5.21nii 694	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))

Syntax hints:  ¬ wn 3   ∧ wa 103   ↔ wb 104   = wceq 1335   ∈ wcel 2128  Vcvv 2712   ∖ cdif 3099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-v 2714  df-dif 3104

This theorem is referenced by:  eldifd  3112  eldifad  3113  eldifbd  3114  difeqri  3228  eldifi  3230  eldifn  3231  difdif  3233  ddifstab  3240  ssconb  3241  sscon  3242  ssdif  3243  raldifb  3248  dfss4st  3341  ssddif  3342  unssdif  3343  inssdif  3344  difin  3345  unssin  3347  inssun  3348  invdif  3350  indif  3351  difundi  3360  difindiss  3362  indifdir  3364  undif3ss  3369  difin2  3370  symdifxor  3374  dfnul2  3397  reldisj  3446  disj3  3447  undif4  3457  ssdif0im  3459  inssdif0im  3462  ssundifim  3478  eldifpr  3588  eldiftp  3607  eldifsn  3688  difprsnss  3696  iundif2ss  3916  iindif2m  3918  brdif  4019  unidif0  4130  eldifpw  4439  elirr  4502  en2lp  4515  difopab  4721  intirr  4974  cnvdif  4994  imadiflem  5251  imadif  5252  elfi2  6918  xrlenlt  7944  nzadd  9224  irradd  9561  irrmul  9562  fzdifsuc  9989  fisumss  11300  prodssdc  11497  fprodssdc  11498  inffinp1  12228  bj-charfunr  13456