![]() |
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 2109 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (𝑥 = 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | 1 | alrimiv 1754 | . 2 ⊢ (𝐴 ∈ 𝐵 → ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵)) |
3 | elisset 2568 | . 2 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 = 𝐴) | |
4 | exim 1490 | . 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥 𝑥 ∈ 𝐵)) | |
5 | 2, 3, 4 | sylc 56 | 1 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1241 = wceq 1243 ∃wex 1381 ∈ wcel 1393 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-sb 1646 df-clab 2027 df-cleq 2033 df-clel 2036 df-v 2559 |
This theorem is referenced by: snmg 3486 oprcl 3573 exss 3963 onintrab2im 4244 regexmidlemm 4257 acexmidlem2 5509 enm 6294 ssfiexmid 6336 fin0 6342 fin0or 6343 diffitest 6344 diffisn 6350 caucvgsrlemasr 6874 gtso 7097 indstr 8536 negm 8550 fzm 8902 fzom 9020 r19.2uz 9591 resqrexlemgt0 9618 climuni 9814 |
Copyright terms: Public domain | W3C validator |