Theorem elin 3126

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 2566	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 2566	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 262	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2100	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2100	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 442	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 2924	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 2689	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 620	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ∧ wa 97   ↔ wb 98   = wceq 1243   ∈ wcel 1393  Vcvv 2557   ∩ cin 2916

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-v 2559  df-in 2924

This theorem is referenced by:  elin2  3127  elin3  3128  incom  3129  ineqri  3130  ineq1  3131  inass  3147  inss1  3157  ssin  3159  ssrin  3162  inssdif  3173  difin  3174  unssin  3176  inssun  3177  invdif  3179  indif  3180  indi  3184  undi  3185  difundi  3189  difindiss  3191  indifdir  3193  difin2  3199  inrab2  3210  inelcm  3282  inssdif0im  3291  uniin  3600  intun  3646  intpr  3647  elrint  3655  iunin2  3720  iinin2m  3725  elriin  3727  brin  3811  trin  3864  inex1  3891  inuni  3909  bnd2  3926  ordpwsucss  4291  ordpwsucexmid  4294  peano5  4321  inopab  4468  inxp  4470  dmin  4543  opelres  4617  intasym  4709  asymref  4710  dminss  4738  imainss  4739  inimasn  4741  ssrnres  4763  cnvresima  4810  dfco2a  4821  imainlem  4980  imain  4981  2elresin  5010  nfvres  5206  respreima  5295  isoini  5457  offval  5719  tfrlem5  5930  peano5nnnn  6966  peano5nni  7917  ixxdisj  8772  icodisj  8860  fzdisj  8916  uzdisj  8955  nn0disj  8995  fzouzdisj  9036  bdinex1  10019  bj-indind  10056  peano5setOLD  10065