ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eldif GIF version

Theorem eldif 3006
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.
StepHypRef Expression
1 elex 2630 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 2630 . . 3 (𝐴𝐵𝐴 ∈ V)
32adantr 270 . 2 ((𝐴𝐵 ∧ ¬ 𝐴𝐶) → 𝐴 ∈ V)
4 eleq1 2150 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
5 eleq1 2150 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
65notbid 627 . . . 4 (𝑥 = 𝐴 → (¬ 𝑥𝐶 ↔ ¬ 𝐴𝐶))
74, 6anbi12d 457 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵 ∧ ¬ 𝑥𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶)))
8 df-dif 2999 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵 ∧ ¬ 𝑥𝐶)}
97, 8elab2g 2760 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶)))
101, 3, 9pm5.21nii 655 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wa 102  wb 103   = wceq 1289  wcel 1438  Vcvv 2619  cdif 2994
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-v 2621  df-dif 2999
This theorem is referenced by:  eldifd  3007  eldifad  3008  eldifbd  3009  difeqri  3118  eldifi  3120  eldifn  3121  difdif  3123  ddifstab  3130  ssconb  3131  sscon  3132  ssdif  3133  raldifb  3138  dfss4st  3230  ssddif  3231  unssdif  3232  inssdif  3233  difin  3234  unssin  3236  inssun  3237  invdif  3239  indif  3240  difundi  3249  difindiss  3251  indifdir  3253  undif3ss  3258  difin2  3259  symdifxor  3263  dfnul2  3286  reldisj  3331  disj3  3332  undif4  3342  ssdif0im  3344  inssdif0im  3347  ssundifim  3362  eldifsn  3562  difprsnss  3570  iundif2ss  3790  iindif2m  3792  brdif  3885  unidif0  3994  eldifpw  4289  elirr  4347  en2lp  4360  difopab  4557  intirr  4805  cnvdif  4825  imadiflem  5079  imadif  5080  xrlenlt  7530  nzadd  8772  irradd  9100  irrmul  9101  fzdifsuc  9462  fisumss  10748
  Copyright terms: Public domain W3C validator