Theorem elin 3172

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

Syntax hints:   ∧ wa 102   ↔ wb 103   = wceq 1287   ∈ wcel 1436  Vcvv 2615   ∩ cin 2987

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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-in 2994

This theorem is referenced by:  elini  3173  elind  3174  elinel1  3175  elinel2  3176  elin2  3177  elin3  3180  incom  3181  ineqri  3182  ineq1  3183  inass  3199  inss1  3209  ssin  3211  ssrin  3214  dfss4st  3221  inssdif  3224  difin  3225  unssin  3227  inssun  3228  invdif  3230  indif  3231  indi  3235  undi  3236  difundi  3240  difindiss  3242  indifdir  3244  difin2  3250  inrab2  3261  inelcm  3331  inssdif0im  3338  uniin  3655  intun  3701  intpr  3702  elrint  3710  iunin2  3775  iinin2m  3780  elriin  3782  brin  3866  trin  3919  inex1  3946  inuni  3964  bnd2  3981  ordpwsucss  4354  ordpwsucexmid  4357  peano5  4384  inopab  4534  inxp  4536  dmin  4610  opelres  4684  intasym  4779  asymref  4780  dminss  4808  imainss  4809  inimasn  4811  ssrnres  4835  cnvresima  4882  dfco2a  4893  funinsn  5024  imainlem  5056  imain  5057  2elresin  5086  nfvres  5293  respreima  5383  isoini  5551  offval  5813  tfrlem5  6026  mapval2  6380  ssenen  6512  fnfi  6589  peano5nnnn  7363  peano5nni  8352  ixxdisj  9245  icodisj  9333  fzdisj  9390  uzdisj  9429  nn0disj  9469  fzouzdisj  9511  isumss  10661  bdinex1  11219  bj-indind  11256