![]() |
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 2261 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (𝑥 = 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | 1 | alrimiv 1885 | . 2 ⊢ (𝐴 ∈ 𝐵 → ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵)) |
3 | elisset 2766 | . 2 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 = 𝐴) | |
4 | exim 1610 | . 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥 𝑥 ∈ 𝐵)) | |
5 | 2, 3, 4 | sylc 62 | 1 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1362 = wceq 1364 ∃wex 1503 ∈ wcel 2160 |
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-5 1458 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-v 2754 |
This theorem is referenced by: snmg 3725 oprcl 3817 brm 4068 ss1o0el1 4215 exss 4245 onintrab2im 4535 regexmidlemm 4549 dmxpid 4866 acexmidlem2 5892 frecabcl 6423 ixpm 6755 enm 6845 ssfilem 6902 fin0 6912 fin0or 6913 diffitest 6914 diffisn 6920 infm 6931 inffiexmid 6933 ctssdc 7141 omct 7145 ctssexmid 7177 exmidfodomrlemr 7230 exmidfodomrlemrALT 7231 exmidaclem 7236 caucvgsrlemasr 7818 suplocsrlempr 7835 gtso 8065 sup3exmid 8943 indstr 9622 negm 9644 fzm 10067 fzom 10193 rexfiuz 11029 r19.2uz 11033 resqrexlemgt0 11060 climuni 11332 bezoutlembi 12037 lcmgcdlem 12108 pcprecl 12320 pc2dvds 12361 4sqlem13m 12434 nninfdclemcl 12498 dfgrp3m 13040 issubg2m 13125 issubgrpd2 13126 issubg3 13128 issubg4m 13129 grpissubg 13130 subgintm 13134 nmzsubg 13146 ghmrn 13193 ghmpreima 13202 dvdsr02 13452 01eq0ring 13533 subrgugrp 13584 lmodfopnelem1 13637 rmodislmodlem 13663 rmodislmod 13664 lss1 13675 lsssubg 13690 islss3 13692 islss4 13695 lss1d 13696 lssintclm 13697 dflidl2rng 13794 lidlsubg 13799 cnsubglem 13879 tgioo 14498 pw1nct 15206 nninfall 15212 |
Copyright terms: Public domain | W3C validator |