Theorem elin 3406

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

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1398   ∈ wcel 2205  Vcvv 2815   ∩ cin 3213

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-in 3220

This theorem is referenced by:  elini  3407  elind  3408  elinel1  3409  elinel2  3410  elin2  3411  elin3  3414  incom  3415  ineqri  3418  ineq1  3419  inass  3435  inss1  3445  ssin  3447  ssrin  3450  dfss4st  3458  inssdif  3461  difin  3462  unssin  3464  inssun  3465  invdif  3467  indif  3468  indi  3472  undi  3473  difundi  3477  difindiss  3479  indifdir  3481  difin2  3487  inrab2  3498  inelcm  3573  inssdif0im  3580  uniin  3939  intun  3985  intpr  3986  elrint  3994  iunin2  4060  iinin2m  4065  elriin  4067  disjnim  4104  disjiun  4109  brin  4167  trin  4223  inex1  4249  inuni  4272  bnd2  4291  ordpwsucss  4694  ordpwsucexmid  4697  peano5  4725  inopab  4892  inxp  4894  dmin  4969  opelres  5048  intasym  5152  asymref  5153  dminss  5182  imainss  5183  inimasn  5185  ssrnres  5210  cnvresima  5257  dfco2a  5268  funinsn  5410  imainlem  5442  imain  5443  2elresin  5474  nfvres  5711  respreima  5810  isoini  5997  offval  6283  tfrlem5  6558  mapval2  6925  ixpin  6971  ssenen  7118  infidc  7214  fnfi  7216  elfpw  7228  peano5nnnn  8223  peano5nni  9257  ixxdisj  10255  icodisj  10344  fzdisj  10406  uzdisj  10449  nn0disj  10494  fzouzdisj  10538  sseqn  11228  hashfibclem  11231  isumss  12102  fsumsplit  12118  sumsplitdc  12143  fsum2dlemstep  12145  fprod2dlemstep  12333  bitsmod  12667  bitsinv1  12673  4sqlem12  13125  ballotfilem2  13172  ballotfilemth  13225  nninfdclemcl  13283  nninfdclemp1  13285  insubm  13740  isrhm  14403  subsubrng2  14461  subsubrg2  14492  2idlelb  14779  isbasis2g  15036  tgval2  15042  tgcl  15055  epttop  15081  ssntr  15113  ntreq0  15123  cnptopresti  15229  cnptoprest  15230  cnptoprest2  15231  lmss  15237  txcnp  15262  txcnmpt  15264  bldisj  15392  blininf  15415  blres  15425  metrest  15497  pilem1  15770  wlk1walkdom  16480  trlsegvdegfi  16588  bj-charfundcALT  16705  bj-charfunr  16706  bdinex1  16795  bj-indind  16828