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 2692 | . 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V) | |
2 | elex 2692 | . . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V) | |
3 | 2 | adantl 275 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V) |
4 | eleq1 2200 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
5 | eleq1 2200 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶)) | |
6 | 4, 5 | anbi12d 464 | . . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))) |
7 | df-in 3072 | . . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)} | |
8 | 6, 7 | elab2g 2826 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))) |
9 | 1, 3, 8 | pm5.21nii 693 | 1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ↔ wb 104 = wceq 1331 ∈ wcel 1480 Vcvv 2681 ∩ cin 3065 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2124 df-cleq 2130 df-clel 2133 df-nfc 2268 df-v 2683 df-in 3072 |
This theorem is referenced by: elini 3255 elind 3256 elinel1 3257 elinel2 3258 elin2 3259 elin3 3262 incom 3263 ineqri 3264 ineq1 3265 inass 3281 inss1 3291 ssin 3293 ssrin 3296 dfss4st 3304 inssdif 3307 difin 3308 unssin 3310 inssun 3311 invdif 3313 indif 3314 indi 3318 undi 3319 difundi 3323 difindiss 3325 indifdir 3327 difin2 3333 inrab2 3344 inelcm 3418 inssdif0im 3425 uniin 3751 intun 3797 intpr 3798 elrint 3806 iunin2 3871 iinin2m 3876 elriin 3878 disjnim 3915 disjiun 3919 brin 3975 trin 4031 inex1 4057 inuni 4075 bnd2 4092 ordpwsucss 4477 ordpwsucexmid 4480 peano5 4507 inopab 4666 inxp 4668 dmin 4742 opelres 4819 intasym 4918 asymref 4919 dminss 4948 imainss 4949 inimasn 4951 ssrnres 4976 cnvresima 5023 dfco2a 5034 funinsn 5167 imainlem 5199 imain 5200 2elresin 5229 nfvres 5447 respreima 5541 isoini 5712 offval 5982 tfrlem5 6204 mapval2 6565 ixpin 6610 ssenen 6738 fnfi 6818 peano5nnnn 7693 peano5nni 8716 ixxdisj 9679 icodisj 9768 fzdisj 9825 uzdisj 9866 nn0disj 9908 fzouzdisj 9950 isumss 11153 fsumsplit 11169 sumsplitdc 11194 fsum2dlemstep 11196 isbasis2g 12201 tgval2 12209 tgcl 12222 epttop 12248 ssntr 12280 ntreq0 12290 cnptopresti 12396 cnptoprest 12397 cnptoprest2 12398 lmss 12404 txcnp 12429 txcnmpt 12431 bldisj 12559 blininf 12582 blres 12592 metrest 12664 pilem1 12849 bdinex1 13086 bj-indind 13119 |
Copyright terms: Public domain | W3C validator |