![]() |
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 2171 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (𝑥 = 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | 1 | alrimiv 1813 | . 2 ⊢ (𝐴 ∈ 𝐵 → ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵)) |
3 | elisset 2655 | . 2 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 = 𝐴) | |
4 | exim 1546 | . 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥 𝑥 ∈ 𝐵)) | |
5 | 2, 3, 4 | sylc 62 | 1 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1297 = wceq 1299 ∃wex 1436 ∈ wcel 1448 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1391 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-ext 2082 |
This theorem depends on definitions: df-bi 116 df-sb 1704 df-clab 2087 df-cleq 2093 df-clel 2096 df-v 2643 |
This theorem is referenced by: snmg 3588 oprcl 3676 exmid01 4061 exss 4087 onintrab2im 4372 regexmidlemm 4385 dmxpid 4698 acexmidlem2 5703 frecabcl 6226 ixpm 6554 enm 6643 ssfilem 6698 fin0 6708 fin0or 6709 diffitest 6710 diffisn 6716 infm 6727 inffiexmid 6729 ctssdc 6912 ctssexmid 6936 exmidfodomrlemr 6967 exmidfodomrlemrALT 6968 caucvgsrlemasr 7485 gtso 7714 sup3exmid 8573 indstr 9238 negm 9257 fzm 9659 fzom 9782 rexfiuz 10601 r19.2uz 10605 resqrexlemgt0 10632 climuni 10901 bezoutlembi 11486 lcmgcdlem 11551 tgioo 12465 nninfall 12788 |
Copyright terms: Public domain | W3C validator |