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

Theorem elin 3156
Description: Expansion of membership in an intersection of two classes. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 29-Apr-1994.)
Assertion
Ref Expression
elin (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))

Proof of Theorem elin
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 elex 2611 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 2611 . . 3 (𝐴𝐶𝐴 ∈ V)
32adantl 271 . 2 ((𝐴𝐵𝐴𝐶) → 𝐴 ∈ V)
4 eleq1 2142 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
5 eleq1 2142 . . . 4 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
64, 5anbi12d 457 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵𝑥𝐶) ↔ (𝐴𝐵𝐴𝐶)))
7 df-in 2980 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵𝑥𝐶)}
86, 7elab2g 2741 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶)))
91, 3, 8pm5.21nii 653 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff set class
Syntax hints:  wa 102  wb 103   = wceq 1285  wcel 1434  Vcvv 2602  cin 2973
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-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-v 2604  df-in 2980
This theorem is referenced by:  elin2  3157  elin3  3158  incom  3159  ineqri  3160  ineq1  3161  inass  3177  inss1  3187  ssin  3189  ssrin  3192  inssdif  3201  difin  3202  unssin  3204  inssun  3205  invdif  3207  indif  3208  indi  3212  undi  3213  difundi  3217  difindiss  3219  indifdir  3221  difin2  3227  inrab2  3238  inelcm  3305  inssdif0im  3312  uniin  3623  intun  3669  intpr  3670  elrint  3678  iunin2  3743  iinin2m  3748  elriin  3750  brin  3834  trin  3887  inex1  3914  inuni  3932  bnd2  3949  ordpwsucss  4312  ordpwsucexmid  4315  peano5  4341  inopab  4490  inxp  4492  dmin  4565  opelres  4639  intasym  4733  asymref  4734  dminss  4762  imainss  4763  inimasn  4765  ssrnres  4787  cnvresima  4834  dfco2a  4845  funinsn  4973  imainlem  5005  imain  5006  2elresin  5035  nfvres  5232  respreima  5321  isoini  5482  offval  5744  tfrlem5  5957  fnfi  6436  peano5nnnn  7109  peano5nni  8098  ixxdisj  8991  icodisj  9079  fzdisj  9136  uzdisj  9175  nn0disj  9214  fzouzdisj  9255  bdinex1  10833  bj-indind  10870
  Copyright terms: Public domain W3C validator