Theorem elin 3387

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

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1395   ∈ wcel 2200  Vcvv 2799   ∩ cin 3196

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-in 3203

This theorem is referenced by:  elini  3388  elind  3389  elinel1  3390  elinel2  3391  elin2  3392  elin3  3395  incom  3396  ineqri  3397  ineq1  3398  inass  3414  inss1  3424  ssin  3426  ssrin  3429  dfss4st  3437  inssdif  3440  difin  3441  unssin  3443  inssun  3444  invdif  3446  indif  3447  indi  3451  undi  3452  difundi  3456  difindiss  3458  indifdir  3460  difin2  3466  inrab2  3477  inelcm  3552  inssdif0im  3559  uniin  3907  intun  3953  intpr  3954  elrint  3962  iunin2  4028  iinin2m  4033  elriin  4035  disjnim  4072  disjiun  4077  brin  4135  trin  4191  inex1  4217  inuni  4238  bnd2  4256  ordpwsucss  4658  ordpwsucexmid  4661  peano5  4689  inopab  4853  inxp  4855  dmin  4930  opelres  5009  intasym  5112  asymref  5113  dminss  5142  imainss  5143  inimasn  5145  ssrnres  5170  cnvresima  5217  dfco2a  5228  funinsn  5369  imainlem  5401  imain  5402  2elresin  5433  nfvres  5662  respreima  5762  isoini  5941  offval  6224  tfrlem5  6458  mapval2  6823  ixpin  6868  ssenen  7008  infidc  7097  fnfi  7099  peano5nnnn  8075  peano5nni  9109  ixxdisj  10095  icodisj  10184  fzdisj  10244  uzdisj  10285  nn0disj  10330  fzouzdisj  10374  isumss  11897  fsumsplit  11913  sumsplitdc  11938  fsum2dlemstep  11940  fprod2dlemstep  12128  bitsmod  12462  bitsinv1  12468  4sqlem12  12920  nninfdclemcl  13014  nninfdclemp1  13016  insubm  13513  isrhm  14116  subsubrng2  14173  subsubrg2  14204  2idlelb  14463  isbasis2g  14713  tgval2  14719  tgcl  14732  epttop  14758  ssntr  14790  ntreq0  14800  cnptopresti  14906  cnptoprest  14907  cnptoprest2  14908  lmss  14914  txcnp  14939  txcnmpt  14941  bldisj  15069  blininf  15092  blres  15102  metrest  15174  pilem1  15447  bj-charfundcALT  16130  bj-charfunr  16131  bdinex1  16220  bj-indind  16253