Theorem elin 3206

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 2652	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 2652	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 273	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2162	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2162	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 460	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 3027	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 2784	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 661	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ∧ wa 103   ↔ wb 104   = wceq 1299   ∈ wcel 1448  Vcvv 2641   ∩ cin 3020

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-v 2643  df-in 3027

This theorem is referenced by:  elini  3207  elind  3208  elinel1  3209  elinel2  3210  elin2  3211  elin3  3214  incom  3215  ineqri  3216  ineq1  3217  inass  3233  inss1  3243  ssin  3245  ssrin  3248  dfss4st  3256  inssdif  3259  difin  3260  unssin  3262  inssun  3263  invdif  3265  indif  3266  indi  3270  undi  3271  difundi  3275  difindiss  3277  indifdir  3279  difin2  3285  inrab2  3296  inelcm  3370  inssdif0im  3377  uniin  3703  intun  3749  intpr  3750  elrint  3758  iunin2  3823  iinin2m  3828  elriin  3830  disjnim  3866  disjiun  3870  brin  3922  trin  3976  inex1  4002  inuni  4020  bnd2  4037  ordpwsucss  4420  ordpwsucexmid  4423  peano5  4450  inopab  4609  inxp  4611  dmin  4685  opelres  4760  intasym  4859  asymref  4860  dminss  4889  imainss  4890  inimasn  4892  ssrnres  4917  cnvresima  4964  dfco2a  4975  funinsn  5108  imainlem  5140  imain  5141  2elresin  5170  nfvres  5386  respreima  5480  isoini  5651  offval  5921  tfrlem5  6141  mapval2  6502  ixpin  6547  ssenen  6674  fnfi  6753  peano5nnnn  7577  peano5nni  8581  ixxdisj  9527  icodisj  9616  fzdisj  9673  uzdisj  9714  nn0disj  9756  fzouzdisj  9798  isumss  10999  fsumsplit  11015  sumsplitdc  11040  fsum2dlemstep  11042  isbasis2g  11994  tgval2  12002  tgcl  12015  epttop  12041  ssntr  12073  ntreq0  12083  cnptopresti  12188  cnptoprest  12189  cnptoprest2  12190  lmss  12196  txcnp  12221  txcnmpt  12223  bldisj  12329  blininf  12352  blres  12362  metrest  12434  bdinex1  12678  bj-indind  12715