![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elex2 | GIF version |
Description: If a class contains another class, then it contains some set. (Contributed by Alan Sare, 25-Sep-2011.) |
Ref | Expression |
---|---|
elex2 | ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1a 2151 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (𝑥 = 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | 1 | alrimiv 1796 | . 2 ⊢ (𝐴 ∈ 𝐵 → ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵)) |
3 | elisset 2614 | . 2 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 = 𝐴) | |
4 | exim 1531 | . 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥 𝑥 ∈ 𝐵)) | |
5 | 2, 3, 4 | sylc 61 | 1 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1283 = wceq 1285 ∃wex 1422 ∈ wcel 1434 |
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-5 1377 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-ext 2064 |
This theorem depends on definitions: df-bi 115 df-sb 1687 df-clab 2069 df-cleq 2075 df-clel 2078 df-v 2604 |
This theorem is referenced by: snmg 3510 oprcl 3596 exss 3984 onintrab2im 4264 regexmidlemm 4277 acexmidlem2 5534 frecabcl 6042 enm 6354 ssfilem 6400 fin0 6409 fin0or 6410 diffitest 6411 diffisn 6417 infm 6422 caucvgsrlemasr 7017 gtso 7246 indstr 8751 negm 8770 fzm 9122 fzom 9239 rexfiuz 10002 r19.2uz 10006 resqrexlemgt0 10033 climuni 10259 bezoutlembi 10527 lcmgcdlem 10592 |
Copyright terms: Public domain | W3C validator |