![]() |
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 2763 | . 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V) | |
2 | elex 2763 | . . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V) | |
3 | 2 | adantl 277 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V) |
4 | eleq1 2252 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
5 | eleq1 2252 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶)) | |
6 | 4, 5 | anbi12d 473 | . . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))) |
7 | df-in 3150 | . . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)} | |
8 | 6, 7 | elab2g 2899 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))) |
9 | 1, 3, 8 | pm5.21nii 705 | 1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 104 ↔ wb 105 = wceq 1364 ∈ wcel 2160 Vcvv 2752 ∩ cin 3143 |
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 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-v 2754 df-in 3150 |
This theorem is referenced by: elini 3334 elind 3335 elinel1 3336 elinel2 3337 elin2 3338 elin3 3341 incom 3342 ineqri 3343 ineq1 3344 inass 3360 inss1 3370 ssin 3372 ssrin 3375 dfss4st 3383 inssdif 3386 difin 3387 unssin 3389 inssun 3390 invdif 3392 indif 3393 indi 3397 undi 3398 difundi 3402 difindiss 3404 indifdir 3406 difin2 3412 inrab2 3423 inelcm 3498 inssdif0im 3505 uniin 3844 intun 3890 intpr 3891 elrint 3899 iunin2 3965 iinin2m 3970 elriin 3972 disjnim 4009 disjiun 4013 brin 4070 trin 4126 inex1 4152 inuni 4173 bnd2 4191 ordpwsucss 4584 ordpwsucexmid 4587 peano5 4615 inopab 4777 inxp 4779 dmin 4853 opelres 4930 intasym 5031 asymref 5032 dminss 5061 imainss 5062 inimasn 5064 ssrnres 5089 cnvresima 5136 dfco2a 5147 funinsn 5284 imainlem 5316 imain 5317 2elresin 5346 nfvres 5568 respreima 5665 isoini 5840 offval 6115 tfrlem5 6340 mapval2 6705 ixpin 6750 ssenen 6880 infidc 6965 fnfi 6967 peano5nnnn 7922 peano5nni 8953 ixxdisj 9935 icodisj 10024 fzdisj 10084 uzdisj 10125 nn0disj 10170 fzouzdisj 10212 isumss 11434 fsumsplit 11450 sumsplitdc 11475 fsum2dlemstep 11477 fprod2dlemstep 11665 4sqlem12 12437 nninfdclemcl 12502 nninfdclemp1 12504 insubm 12952 isrhm 13525 subsubrng2 13579 subsubrg2 13610 2idlelb 13837 isbasis2g 14022 tgval2 14028 tgcl 14041 epttop 14067 ssntr 14099 ntreq0 14109 cnptopresti 14215 cnptoprest 14216 cnptoprest2 14217 lmss 14223 txcnp 14248 txcnmpt 14250 bldisj 14378 blininf 14401 blres 14411 metrest 14483 pilem1 14677 bj-charfundcALT 15039 bj-charfunr 15040 bdinex1 15129 bj-indind 15162 |
Copyright terms: Public domain | W3C validator |