Theorem elin 3305

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.

Step	Hyp	Ref	Expression
1		elex 2737	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 2737	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 275	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2229	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2229	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 465	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 3122	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 2873	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 694	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ∧ wa 103   ↔ wb 104   = wceq 1343   ∈ wcel 2136  Vcvv 2726   ∩ cin 3115

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 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-v 2728  df-in 3122

This theorem is referenced by:  elini  3306  elind  3307  elinel1  3308  elinel2  3309  elin2  3310  elin3  3313  incom  3314  ineqri  3315  ineq1  3316  inass  3332  inss1  3342  ssin  3344  ssrin  3347  dfss4st  3355  inssdif  3358  difin  3359  unssin  3361  inssun  3362  invdif  3364  indif  3365  indi  3369  undi  3370  difundi  3374  difindiss  3376  indifdir  3378  difin2  3384  inrab2  3395  inelcm  3469  inssdif0im  3476  uniin  3809  intun  3855  intpr  3856  elrint  3864  iunin2  3929  iinin2m  3934  elriin  3936  disjnim  3973  disjiun  3977  brin  4034  trin  4090  inex1  4116  inuni  4134  bnd2  4152  ordpwsucss  4544  ordpwsucexmid  4547  peano5  4575  inopab  4736  inxp  4738  dmin  4812  opelres  4889  intasym  4988  asymref  4989  dminss  5018  imainss  5019  inimasn  5021  ssrnres  5046  cnvresima  5093  dfco2a  5104  funinsn  5237  imainlem  5269  imain  5270  2elresin  5299  nfvres  5519  respreima  5613  isoini  5786  offval  6057  tfrlem5  6282  mapval2  6644  ixpin  6689  ssenen  6817  fnfi  6902  peano5nnnn  7833  peano5nni  8860  ixxdisj  9839  icodisj  9928  fzdisj  9987  uzdisj  10028  nn0disj  10073  fzouzdisj  10115  isumss  11332  fsumsplit  11348  sumsplitdc  11373  fsum2dlemstep  11375  fprod2dlemstep  11563  nninfdclemcl  12381  nninfdclemp1  12383  isbasis2g  12683  tgval2  12691  tgcl  12704  epttop  12730  ssntr  12762  ntreq0  12772  cnptopresti  12878  cnptoprest  12879  cnptoprest2  12880  lmss  12886  txcnp  12911  txcnmpt  12913  bldisj  13041  blininf  13064  blres  13074  metrest  13146  pilem1  13340  bj-charfundcALT  13691  bj-charfunr  13692  bdinex1  13781  bj-indind  13814