Theorem elin 3346

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  3347  elind  3348  elinel1  3349  elinel2  3350  elin2  3351  elin3  3354  incom  3355  ineqri  3356  ineq1  3357  inass  3373  inss1  3383  ssin  3385  ssrin  3388  dfss4st  3396  inssdif  3399  difin  3400  unssin  3402  inssun  3403  invdif  3405  indif  3406  indi  3410  undi  3411  difundi  3415  difindiss  3417  indifdir  3419  difin2  3425  inrab2  3436  inelcm  3511  inssdif0im  3518  uniin  3859  intun  3905  intpr  3906  elrint  3914  iunin2  3980  iinin2m  3985  elriin  3987  disjnim  4024  disjiun  4028  brin  4085  trin  4141  inex1  4167  inuni  4188  bnd2  4206  ordpwsucss  4603  ordpwsucexmid  4606  peano5  4634  inopab  4798  inxp  4800  dmin  4874  opelres  4951  intasym  5054  asymref  5055  dminss  5084  imainss  5085  inimasn  5087  ssrnres  5112  cnvresima  5159  dfco2a  5170  funinsn  5307  imainlem  5339  imain  5340  2elresin  5369  nfvres  5592  respreima  5690  isoini  5865  offval  6143  tfrlem5  6372  mapval2  6737  ixpin  6782  ssenen  6912  infidc  7000  fnfi  7002  peano5nnnn  7959  peano5nni  8993  ixxdisj  9978  icodisj  10067  fzdisj  10127  uzdisj  10168  nn0disj  10213  fzouzdisj  10256  isumss  11556  fsumsplit  11572  sumsplitdc  11597  fsum2dlemstep  11599  fprod2dlemstep  11787  4sqlem12  12571  nninfdclemcl  12665  nninfdclemp1  12667  insubm  13117  isrhm  13714  subsubrng2  13771  subsubrg2  13802  2idlelb  14061  isbasis2g  14281  tgval2  14287  tgcl  14300  epttop  14326  ssntr  14358  ntreq0  14368  cnptopresti  14474  cnptoprest  14475  cnptoprest2  14476  lmss  14482  txcnp  14507  txcnmpt  14509  bldisj  14637  blininf  14660  blres  14670  metrest  14742  pilem1  15015  bj-charfundcALT  15455  bj-charfunr  15456  bdinex1  15545  bj-indind  15578