Theorem elin 3364

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

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1373   ∈ wcel 2178  Vcvv 2776   ∩ cin 3173

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-in 3180

This theorem is referenced by:  elini  3365  elind  3366  elinel1  3367  elinel2  3368  elin2  3369  elin3  3372  incom  3373  ineqri  3374  ineq1  3375  inass  3391  inss1  3401  ssin  3403  ssrin  3406  dfss4st  3414  inssdif  3417  difin  3418  unssin  3420  inssun  3421  invdif  3423  indif  3424  indi  3428  undi  3429  difundi  3433  difindiss  3435  indifdir  3437  difin2  3443  inrab2  3454  inelcm  3529  inssdif0im  3536  uniin  3884  intun  3930  intpr  3931  elrint  3939  iunin2  4005  iinin2m  4010  elriin  4012  disjnim  4049  disjiun  4054  brin  4112  trin  4168  inex1  4194  inuni  4215  bnd2  4233  ordpwsucss  4633  ordpwsucexmid  4636  peano5  4664  inopab  4828  inxp  4830  dmin  4905  opelres  4983  intasym  5086  asymref  5087  dminss  5116  imainss  5117  inimasn  5119  ssrnres  5144  cnvresima  5191  dfco2a  5202  funinsn  5342  imainlem  5374  imain  5375  2elresin  5406  nfvres  5633  respreima  5731  isoini  5910  offval  6189  tfrlem5  6423  mapval2  6788  ixpin  6833  ssenen  6973  infidc  7062  fnfi  7064  peano5nnnn  8040  peano5nni  9074  ixxdisj  10060  icodisj  10149  fzdisj  10209  uzdisj  10250  nn0disj  10295  fzouzdisj  10339  isumss  11817  fsumsplit  11833  sumsplitdc  11858  fsum2dlemstep  11860  fprod2dlemstep  12048  bitsmod  12382  bitsinv1  12388  4sqlem12  12840  nninfdclemcl  12934  nninfdclemp1  12936  insubm  13432  isrhm  14035  subsubrng2  14092  subsubrg2  14123  2idlelb  14382  isbasis2g  14632  tgval2  14638  tgcl  14651  epttop  14677  ssntr  14709  ntreq0  14719  cnptopresti  14825  cnptoprest  14826  cnptoprest2  14827  lmss  14833  txcnp  14858  txcnmpt  14860  bldisj  14988  blininf  15011  blres  15021  metrest  15093  pilem1  15366  bj-charfundcALT  15944  bj-charfunr  15945  bdinex1  16034  bj-indind  16067