Theorem elin 3156

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 2611	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 2611	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 271	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2142	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2142	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 457	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 2980	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 2741	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 653	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ∧ wa 102   ↔ wb 103   = wceq 1285   ∈ wcel 1434  Vcvv 2602   ∩ cin 2973

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-v 2604  df-in 2980

This theorem is referenced by:  elin2  3157  elin3  3158  incom  3159  ineqri  3160  ineq1  3161  inass  3177  inss1  3187  ssin  3189  ssrin  3192  inssdif  3201  difin  3202  unssin  3204  inssun  3205  invdif  3207  indif  3208  indi  3212  undi  3213  difundi  3217  difindiss  3219  indifdir  3221  difin2  3227  inrab2  3238  inelcm  3305  inssdif0im  3312  uniin  3623  intun  3669  intpr  3670  elrint  3678  iunin2  3743  iinin2m  3748  elriin  3750  brin  3834  trin  3887  inex1  3914  inuni  3932  bnd2  3949  ordpwsucss  4312  ordpwsucexmid  4315  peano5  4341  inopab  4490  inxp  4492  dmin  4565  opelres  4639  intasym  4733  asymref  4734  dminss  4762  imainss  4763  inimasn  4765  ssrnres  4787  cnvresima  4834  dfco2a  4845  funinsn  4973  imainlem  5005  imain  5006  2elresin  5035  nfvres  5232  respreima  5321  isoini  5482  offval  5744  tfrlem5  5957  fnfi  6436  peano5nnnn  7109  peano5nni  8098  ixxdisj  8991  icodisj  9079  fzdisj  9136  uzdisj  9175  nn0disj  9214  fzouzdisj  9255  bdinex1  10833  bj-indind  10870