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  7978  peano5nni  9012  ixxdisj  9997  icodisj  10086  fzdisj  10146  uzdisj  10187  nn0disj  10232  fzouzdisj  10275  isumss  11575  fsumsplit  11591  sumsplitdc  11616  fsum2dlemstep  11618  fprod2dlemstep  11806  bitsmod  12140  bitsinv1  12146  4sqlem12  12598  nninfdclemcl  12692  nninfdclemp1  12694  insubm  13189  isrhm  13792  subsubrng2  13849  subsubrg2  13880  2idlelb  14139  isbasis2g  14389  tgval2  14395  tgcl  14408  epttop  14434  ssntr  14466  ntreq0  14476  cnptopresti  14582  cnptoprest  14583  cnptoprest2  14584  lmss  14590  txcnp  14615  txcnmpt  14617  bldisj  14745  blininf  14768  blres  14778  metrest  14850  pilem1  15123  bj-charfundcALT  15563  bj-charfunr  15564  bdinex1  15653  bj-indind  15686