Theorem elin 3310

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 2741	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 2741	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 275	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2233	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2233	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 470	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 3127	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 2877	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 699	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ∧ wa 103   ↔ wb 104   = wceq 1348   ∈ wcel 2141  Vcvv 2730   ∩ cin 3120

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-in 3127

This theorem is referenced by:  elini  3311  elind  3312  elinel1  3313  elinel2  3314  elin2  3315  elin3  3318  incom  3319  ineqri  3320  ineq1  3321  inass  3337  inss1  3347  ssin  3349  ssrin  3352  dfss4st  3360  inssdif  3363  difin  3364  unssin  3366  inssun  3367  invdif  3369  indif  3370  indi  3374  undi  3375  difundi  3379  difindiss  3381  indifdir  3383  difin2  3389  inrab2  3400  inelcm  3475  inssdif0im  3482  uniin  3816  intun  3862  intpr  3863  elrint  3871  iunin2  3936  iinin2m  3941  elriin  3943  disjnim  3980  disjiun  3984  brin  4041  trin  4097  inex1  4123  inuni  4141  bnd2  4159  ordpwsucss  4551  ordpwsucexmid  4554  peano5  4582  inopab  4743  inxp  4745  dmin  4819  opelres  4896  intasym  4995  asymref  4996  dminss  5025  imainss  5026  inimasn  5028  ssrnres  5053  cnvresima  5100  dfco2a  5111  funinsn  5247  imainlem  5279  imain  5280  2elresin  5309  nfvres  5529  respreima  5624  isoini  5797  offval  6068  tfrlem5  6293  mapval2  6656  ixpin  6701  ssenen  6829  fnfi  6914  peano5nnnn  7854  peano5nni  8881  ixxdisj  9860  icodisj  9949  fzdisj  10008  uzdisj  10049  nn0disj  10094  fzouzdisj  10136  isumss  11354  fsumsplit  11370  sumsplitdc  11395  fsum2dlemstep  11397  fprod2dlemstep  11585  nninfdclemcl  12403  nninfdclemp1  12405  insubm  12703  isbasis2g  12837  tgval2  12845  tgcl  12858  epttop  12884  ssntr  12916  ntreq0  12926  cnptopresti  13032  cnptoprest  13033  cnptoprest2  13034  lmss  13040  txcnp  13065  txcnmpt  13067  bldisj  13195  blininf  13218  blres  13228  metrest  13300  pilem1  13494  bj-charfundcALT  13844  bj-charfunr  13845  bdinex1  13934  bj-indind  13967