![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elin | GIF version |
Description: Expansion of membership in an intersection of two classes. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 29-Apr-1994.) |
Ref | Expression |
---|---|
elin | ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 2652 | . 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V) | |
2 | elex 2652 | . . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V) | |
3 | 2 | adantl 273 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V) |
4 | eleq1 2162 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
5 | eleq1 2162 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶)) | |
6 | 4, 5 | anbi12d 460 | . . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))) |
7 | df-in 3027 | . . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)} | |
8 | 6, 7 | elab2g 2784 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))) |
9 | 1, 3, 8 | pm5.21nii 661 | 1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ↔ wb 104 = wceq 1299 ∈ wcel 1448 Vcvv 2641 ∩ cin 3020 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 |
This theorem depends on definitions: df-bi 116 df-tru 1302 df-nf 1405 df-sb 1704 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-v 2643 df-in 3027 |
This theorem is referenced by: elini 3207 elind 3208 elinel1 3209 elinel2 3210 elin2 3211 elin3 3214 incom 3215 ineqri 3216 ineq1 3217 inass 3233 inss1 3243 ssin 3245 ssrin 3248 dfss4st 3256 inssdif 3259 difin 3260 unssin 3262 inssun 3263 invdif 3265 indif 3266 indi 3270 undi 3271 difundi 3275 difindiss 3277 indifdir 3279 difin2 3285 inrab2 3296 inelcm 3370 inssdif0im 3377 uniin 3703 intun 3749 intpr 3750 elrint 3758 iunin2 3823 iinin2m 3828 elriin 3830 disjnim 3866 disjiun 3870 brin 3922 trin 3976 inex1 4002 inuni 4020 bnd2 4037 ordpwsucss 4420 ordpwsucexmid 4423 peano5 4450 inopab 4609 inxp 4611 dmin 4685 opelres 4760 intasym 4859 asymref 4860 dminss 4889 imainss 4890 inimasn 4892 ssrnres 4917 cnvresima 4964 dfco2a 4975 funinsn 5108 imainlem 5140 imain 5141 2elresin 5170 nfvres 5386 respreima 5480 isoini 5651 offval 5921 tfrlem5 6141 mapval2 6502 ixpin 6547 ssenen 6674 fnfi 6753 peano5nnnn 7577 peano5nni 8581 ixxdisj 9527 icodisj 9616 fzdisj 9673 uzdisj 9714 nn0disj 9756 fzouzdisj 9798 isumss 10999 fsumsplit 11015 sumsplitdc 11040 fsum2dlemstep 11042 isbasis2g 11994 tgval2 12002 tgcl 12015 epttop 12041 ssntr 12073 ntreq0 12083 cnptopresti 12188 cnptoprest 12189 cnptoprest2 12190 lmss 12196 txcnp 12221 txcnmpt 12223 bldisj 12329 blininf 12352 blres 12362 metrest 12434 bdinex1 12678 bj-indind 12715 |
Copyright terms: Public domain | W3C validator |