Theorem elin 3347

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 2774	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 2774	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 277	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2259	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2259	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 473	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 3163	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 2911	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 705	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1364   ∈ wcel 2167  Vcvv 2763   ∩ cin 3156

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-in 3163

This theorem is referenced by:  elini  3348  elind  3349  elinel1  3350  elinel2  3351  elin2  3352  elin3  3355  incom  3356  ineqri  3357  ineq1  3358  inass  3374  inss1  3384  ssin  3386  ssrin  3389  dfss4st  3397  inssdif  3400  difin  3401  unssin  3403  inssun  3404  invdif  3406  indif  3407  indi  3411  undi  3412  difundi  3416  difindiss  3418  indifdir  3420  difin2  3426  inrab2  3437  inelcm  3512  inssdif0im  3519  uniin  3860  intun  3906  intpr  3907  elrint  3915  iunin2  3981  iinin2m  3986  elriin  3988  disjnim  4025  disjiun  4029  brin  4086  trin  4142  inex1  4168  inuni  4189  bnd2  4207  ordpwsucss  4604  ordpwsucexmid  4607  peano5  4635  inopab  4799  inxp  4801  dmin  4875  opelres  4952  intasym  5055  asymref  5056  dminss  5085  imainss  5086  inimasn  5088  ssrnres  5113  cnvresima  5160  dfco2a  5171  funinsn  5308  imainlem  5340  imain  5341  2elresin  5372  nfvres  5595  respreima  5693  isoini  5868  offval  6147  tfrlem5  6381  mapval2  6746  ixpin  6791  ssenen  6921  infidc  7009  fnfi  7011  peano5nnnn  7976  peano5nni  9010  ixxdisj  9995  icodisj  10084  fzdisj  10144  uzdisj  10185  nn0disj  10230  fzouzdisj  10273  isumss  11573  fsumsplit  11589  sumsplitdc  11614  fsum2dlemstep  11616  fprod2dlemstep  11804  bitsmod  12138  bitsinv1  12144  4sqlem12  12596  nninfdclemcl  12690  nninfdclemp1  12692  insubm  13187  isrhm  13790  subsubrng2  13847  subsubrg2  13878  2idlelb  14137  isbasis2g  14365  tgval2  14371  tgcl  14384  epttop  14410  ssntr  14442  ntreq0  14452  cnptopresti  14558  cnptoprest  14559  cnptoprest2  14560  lmss  14566  txcnp  14591  txcnmpt  14593  bldisj  14721  blininf  14744  blres  14754  metrest  14826  pilem1  15099  bj-charfundcALT  15539  bj-charfunr  15540  bdinex1  15629  bj-indind  15662