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

Theorem elin 3172
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 2624 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 2624 . . 3 (𝐴𝐶𝐴 ∈ V)
32adantl 271 . 2 ((𝐴𝐵𝐴𝐶) → 𝐴 ∈ V)
4 eleq1 2147 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
5 eleq1 2147 . . . 4 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
64, 5anbi12d 457 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵𝑥𝐶) ↔ (𝐴𝐵𝐴𝐶)))
7 df-in 2994 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵𝑥𝐶)}
86, 7elab2g 2753 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶)))
91, 3, 8pm5.21nii 653 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff set class
Syntax hints:  wa 102  wb 103   = wceq 1287  wcel 1436  Vcvv 2615  cin 2987
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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-in 2994
This theorem is referenced by:  elini  3173  elind  3174  elinel1  3175  elinel2  3176  elin2  3177  elin3  3180  incom  3181  ineqri  3182  ineq1  3183  inass  3199  inss1  3209  ssin  3211  ssrin  3214  dfss4st  3221  inssdif  3224  difin  3225  unssin  3227  inssun  3228  invdif  3230  indif  3231  indi  3235  undi  3236  difundi  3240  difindiss  3242  indifdir  3244  difin2  3250  inrab2  3261  inelcm  3331  inssdif0im  3338  uniin  3655  intun  3701  intpr  3702  elrint  3710  iunin2  3775  iinin2m  3780  elriin  3782  brin  3866  trin  3919  inex1  3946  inuni  3964  bnd2  3981  ordpwsucss  4354  ordpwsucexmid  4357  peano5  4384  inopab  4534  inxp  4536  dmin  4610  opelres  4684  intasym  4779  asymref  4780  dminss  4808  imainss  4809  inimasn  4811  ssrnres  4835  cnvresima  4882  dfco2a  4893  funinsn  5024  imainlem  5056  imain  5057  2elresin  5086  nfvres  5293  respreima  5383  isoini  5551  offval  5813  tfrlem5  6026  mapval2  6380  ssenen  6512  fnfi  6589  peano5nnnn  7363  peano5nni  8352  ixxdisj  9245  icodisj  9333  fzdisj  9390  uzdisj  9429  nn0disj  9469  fzouzdisj  9511  isumss  10661  bdinex1  11219  bj-indind  11256
  Copyright terms: Public domain W3C validator