Theorem eldif 3175

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 2783	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ V)
2		elex 2783	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 276	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2268	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2268	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	5	notbid 669	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ 𝐶 ↔ ¬ 𝐴 ∈ 𝐶))
7	4, 6	anbi12d 473	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
8		df-dif 3168	. . 3 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)}
9	7, 8	elab2g 2920	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶)))
10	1, 3, 9	pm5.21nii 706	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))

Syntax hints:  ¬ wn 3   ∧ wa 104   ↔ wb 105   = wceq 1373   ∈ wcel 2176  Vcvv 2772   ∖ cdif 3163

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-dif 3168

This theorem is referenced by:  eldifd  3176  eldifad  3177  eldifbd  3178  difeqri  3293  eldifi  3295  eldifn  3296  difdif  3298  ddifstab  3305  ssconb  3306  sscon  3307  ssdif  3308  raldifb  3313  dfss4st  3406  ssddif  3407  unssdif  3408  inssdif  3409  difin  3410  unssin  3412  inssun  3413  invdif  3415  indif  3416  difundi  3425  difindiss  3427  indifdir  3429  undif3ss  3434  difin2  3435  symdifxor  3439  dfnul2  3462  reldisj  3512  disj3  3513  undif4  3523  ssdif0im  3525  inssdif0im  3528  ssundifim  3544  eldifpr  3660  eldiftp  3679  eldifsn  3760  difprsnss  3771  iundif2ss  3993  iindif2m  3995  brdif  4097  unidif0  4211  eldifpw  4524  elirr  4589  en2lp  4602  difopab  4811  intirr  5069  cnvdif  5089  imadiflem  5353  imadif  5354  elfi2  7074  xrlenlt  8137  nzadd  9425  irradd  9767  irrmul  9768  fzdifsuc  10203  fisumss  11703  prodssdc  11900  fprodssdc  11901  bitscmp  12269  inffinp1  12800  bj-charfunr  15746