Theorem elin 3333

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

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1364   ∈ wcel 2160  Vcvv 2752   ∩ cin 3143

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-in 3150

This theorem is referenced by:  elini  3334  elind  3335  elinel1  3336  elinel2  3337  elin2  3338  elin3  3341  incom  3342  ineqri  3343  ineq1  3344  inass  3360  inss1  3370  ssin  3372  ssrin  3375  dfss4st  3383  inssdif  3386  difin  3387  unssin  3389  inssun  3390  invdif  3392  indif  3393  indi  3397  undi  3398  difundi  3402  difindiss  3404  indifdir  3406  difin2  3412  inrab2  3423  inelcm  3498  inssdif0im  3505  uniin  3844  intun  3890  intpr  3891  elrint  3899  iunin2  3965  iinin2m  3970  elriin  3972  disjnim  4009  disjiun  4013  brin  4070  trin  4126  inex1  4152  inuni  4173  bnd2  4191  ordpwsucss  4584  ordpwsucexmid  4587  peano5  4615  inopab  4777  inxp  4779  dmin  4853  opelres  4930  intasym  5031  asymref  5032  dminss  5061  imainss  5062  inimasn  5064  ssrnres  5089  cnvresima  5136  dfco2a  5147  funinsn  5284  imainlem  5316  imain  5317  2elresin  5346  nfvres  5568  respreima  5665  isoini  5840  offval  6115  tfrlem5  6340  mapval2  6705  ixpin  6750  ssenen  6880  infidc  6965  fnfi  6967  peano5nnnn  7922  peano5nni  8953  ixxdisj  9935  icodisj  10024  fzdisj  10084  uzdisj  10125  nn0disj  10170  fzouzdisj  10212  isumss  11434  fsumsplit  11450  sumsplitdc  11475  fsum2dlemstep  11477  fprod2dlemstep  11665  4sqlem12  12437  nninfdclemcl  12502  nninfdclemp1  12504  insubm  12952  isrhm  13525  subsubrng2  13579  subsubrg2  13610  2idlelb  13837  isbasis2g  14022  tgval2  14028  tgcl  14041  epttop  14067  ssntr  14099  ntreq0  14109  cnptopresti  14215  cnptoprest  14216  cnptoprest2  14217  lmss  14223  txcnp  14248  txcnmpt  14250  bldisj  14378  blininf  14401  blres  14411  metrest  14483  pilem1  14677  bj-charfundcALT  15039  bj-charfunr  15040  bdinex1  15129  bj-indind  15162