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

Theorem elin 3229
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 2671 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 2671 . . 3 (𝐴𝐶𝐴 ∈ V)
32adantl 275 . 2 ((𝐴𝐵𝐴𝐶) → 𝐴 ∈ V)
4 eleq1 2180 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
5 eleq1 2180 . . . 4 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
64, 5anbi12d 464 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵𝑥𝐶) ↔ (𝐴𝐵𝐴𝐶)))
7 df-in 3047 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵𝑥𝐶)}
86, 7elab2g 2804 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶)))
91, 3, 8pm5.21nii 678 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff set class
Syntax hints:  wa 103  wb 104   = wceq 1316  wcel 1465  Vcvv 2660  cin 3040
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-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-v 2662  df-in 3047
This theorem is referenced by:  elini  3230  elind  3231  elinel1  3232  elinel2  3233  elin2  3234  elin3  3237  incom  3238  ineqri  3239  ineq1  3240  inass  3256  inss1  3266  ssin  3268  ssrin  3271  dfss4st  3279  inssdif  3282  difin  3283  unssin  3285  inssun  3286  invdif  3288  indif  3289  indi  3293  undi  3294  difundi  3298  difindiss  3300  indifdir  3302  difin2  3308  inrab2  3319  inelcm  3393  inssdif0im  3400  uniin  3726  intun  3772  intpr  3773  elrint  3781  iunin2  3846  iinin2m  3851  elriin  3853  disjnim  3890  disjiun  3894  brin  3950  trin  4006  inex1  4032  inuni  4050  bnd2  4067  ordpwsucss  4452  ordpwsucexmid  4455  peano5  4482  inopab  4641  inxp  4643  dmin  4717  opelres  4794  intasym  4893  asymref  4894  dminss  4923  imainss  4924  inimasn  4926  ssrnres  4951  cnvresima  4998  dfco2a  5009  funinsn  5142  imainlem  5174  imain  5175  2elresin  5204  nfvres  5422  respreima  5516  isoini  5687  offval  5957  tfrlem5  6179  mapval2  6540  ixpin  6585  ssenen  6713  fnfi  6793  peano5nnnn  7668  peano5nni  8691  ixxdisj  9654  icodisj  9743  fzdisj  9800  uzdisj  9841  nn0disj  9883  fzouzdisj  9925  isumss  11128  fsumsplit  11144  sumsplitdc  11169  fsum2dlemstep  11171  isbasis2g  12139  tgval2  12147  tgcl  12160  epttop  12186  ssntr  12218  ntreq0  12228  cnptopresti  12334  cnptoprest  12335  cnptoprest2  12336  lmss  12342  txcnp  12367  txcnmpt  12369  bldisj  12497  blininf  12520  blres  12530  metrest  12602  pilem1  12787  bdinex1  13024  bj-indind  13057
  Copyright terms: Public domain W3C validator