Theorem elin 3402

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

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1398   ∈ wcel 2203  Vcvv 2813   ∩ cin 3210

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-in 3217

This theorem is referenced by:  elini  3403  elind  3404  elinel1  3405  elinel2  3406  elin2  3407  elin3  3410  incom  3411  ineqri  3414  ineq1  3415  inass  3431  inss1  3441  ssin  3443  ssrin  3446  dfss4st  3454  inssdif  3457  difin  3458  unssin  3460  inssun  3461  invdif  3463  indif  3464  indi  3468  undi  3469  difundi  3473  difindiss  3475  indifdir  3477  difin2  3483  inrab2  3494  inelcm  3569  inssdif0im  3576  uniin  3934  intun  3980  intpr  3981  elrint  3989  iunin2  4055  iinin2m  4060  elriin  4062  disjnim  4099  disjiun  4104  brin  4162  trin  4218  inex1  4244  inuni  4267  bnd2  4286  ordpwsucss  4689  ordpwsucexmid  4692  peano5  4720  inopab  4887  inxp  4889  dmin  4964  opelres  5043  intasym  5147  asymref  5148  dminss  5177  imainss  5178  inimasn  5180  ssrnres  5205  cnvresima  5252  dfco2a  5263  funinsn  5405  imainlem  5437  imain  5438  2elresin  5469  nfvres  5706  respreima  5805  isoini  5991  offval  6274  tfrlem5  6545  mapval2  6912  ixpin  6958  ssenen  7105  infidc  7201  fnfi  7203  elfpw  7215  peano5nnnn  8207  peano5nni  9240  ixxdisj  10236  icodisj  10325  fzdisj  10386  uzdisj  10427  nn0disj  10472  fzouzdisj  10516  sseqn  11203  hashfibclem  11206  isumss  12077  fsumsplit  12093  sumsplitdc  12118  fsum2dlemstep  12120  fprod2dlemstep  12308  bitsmod  12642  bitsinv1  12648  4sqlem12  13100  ballotfilem2  13142  nninfdclemcl  13199  nninfdclemp1  13201  insubm  13698  isrhm  14303  subsubrng2  14360  subsubrg2  14391  2idlelb  14653  isbasis2g  14910  tgval2  14916  tgcl  14929  epttop  14955  ssntr  14987  ntreq0  14997  cnptopresti  15103  cnptoprest  15104  cnptoprest2  15105  lmss  15111  txcnp  15136  txcnmpt  15138  bldisj  15266  blininf  15289  blres  15299  metrest  15371  pilem1  15644  wlk1walkdom  16354  trlsegvdegfi  16462  bj-charfundcALT  16579  bj-charfunr  16580  bdinex1  16669  bj-indind  16702