![]() |
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 2611 | . 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V) | |
2 | elex 2611 | . . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V) | |
3 | 2 | adantl 271 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V) |
4 | eleq1 2142 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
5 | eleq1 2142 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶)) | |
6 | 4, 5 | anbi12d 457 | . . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))) |
7 | df-in 2980 | . . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)} | |
8 | 6, 7 | elab2g 2741 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))) |
9 | 1, 3, 8 | pm5.21nii 653 | 1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 102 ↔ wb 103 = wceq 1285 ∈ wcel 1434 Vcvv 2602 ∩ cin 2973 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2064 |
This theorem depends on definitions: df-bi 115 df-tru 1288 df-nf 1391 df-sb 1687 df-clab 2069 df-cleq 2075 df-clel 2078 df-nfc 2209 df-v 2604 df-in 2980 |
This theorem is referenced by: elin2 3157 elin3 3158 incom 3159 ineqri 3160 ineq1 3161 inass 3177 inss1 3187 ssin 3189 ssrin 3192 inssdif 3201 difin 3202 unssin 3204 inssun 3205 invdif 3207 indif 3208 indi 3212 undi 3213 difundi 3217 difindiss 3219 indifdir 3221 difin2 3227 inrab2 3238 inelcm 3305 inssdif0im 3312 uniin 3623 intun 3669 intpr 3670 elrint 3678 iunin2 3743 iinin2m 3748 elriin 3750 brin 3834 trin 3887 inex1 3914 inuni 3932 bnd2 3949 ordpwsucss 4312 ordpwsucexmid 4315 peano5 4341 inopab 4490 inxp 4492 dmin 4565 opelres 4639 intasym 4733 asymref 4734 dminss 4762 imainss 4763 inimasn 4765 ssrnres 4787 cnvresima 4834 dfco2a 4845 funinsn 4973 imainlem 5005 imain 5006 2elresin 5035 nfvres 5232 respreima 5321 isoini 5482 offval 5744 tfrlem5 5957 fnfi 6436 peano5nnnn 7109 peano5nni 8098 ixxdisj 8991 icodisj 9079 fzdisj 9136 uzdisj 9175 nn0disj 9214 fzouzdisj 9255 bdinex1 10833 bj-indind 10870 |
Copyright terms: Public domain | W3C validator |