Theorem elin 3151

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 2581	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 2581	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 266	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2114	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2114	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 450	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 2949	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 2709	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 628	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ∧ wa 101   ↔ wb 102   = wceq 1257   ∈ wcel 1407  Vcvv 2572   ∩ cin 2941

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 638  ax-5 1350  ax-7 1351  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-8 1409  ax-10 1410  ax-11 1411  ax-i12 1412  ax-bndl 1413  ax-4 1414  ax-17 1433  ax-i9 1437  ax-ial 1441  ax-i5r 1442  ax-ext 2036

This theorem depends on definitions:  df-bi 114  df-tru 1260  df-nf 1364  df-sb 1660  df-clab 2041  df-cleq 2047  df-clel 2050  df-nfc 2181  df-v 2574  df-in 2949

This theorem is referenced by:  elin2  3152  elin3  3153  incom  3154  ineqri  3155  ineq1  3156  inass  3172  inss1  3182  ssin  3184  ssrin  3187  inssdif  3198  difin  3199  unssin  3201  inssun  3202  invdif  3204  indif  3205  indi  3209  undi  3210  difundi  3214  difindiss  3216  indifdir  3218  difin2  3224  inrab2  3235  inelcm  3307  inssdif0im  3316  uniin  3625  intun  3671  intpr  3672  elrint  3680  iunin2  3745  iinin2m  3750  elriin  3752  brin  3836  trin  3889  inex1  3916  inuni  3934  bnd2  3951  ordpwsucss  4316  ordpwsucexmid  4319  peano5  4346  inopab  4493  inxp  4495  dmin  4568  opelres  4642  intasym  4734  asymref  4735  dminss  4763  imainss  4764  inimasn  4766  ssrnres  4788  cnvresima  4835  dfco2a  4846  imainlem  5005  imain  5006  2elresin  5035  nfvres  5231  respreima  5320  isoini  5482  offval  5744  tfrlem5  5958  peano5nnnn  6994  peano5nni  7963  ixxdisj  8843  icodisj  8931  fzdisj  8988  uzdisj  9027  nn0disj  9067  fzouzdisj  9108  bdinex1  10349  bj-indind  10386  peano5setOLD  10395