Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  elex2 GIF version

Theorem elex2 2570
 Description: If a class contains another class, then it contains some set. (Contributed by Alan Sare, 25-Sep-2011.)
Assertion
Ref Expression
elex2 (𝐴𝐵 → ∃𝑥 𝑥𝐵)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem elex2
StepHypRef Expression
1 eleq1a 2109 . . 3 (𝐴𝐵 → (𝑥 = 𝐴𝑥𝐵))
21alrimiv 1754 . 2 (𝐴𝐵 → ∀𝑥(𝑥 = 𝐴𝑥𝐵))
3 elisset 2568 . 2 (𝐴𝐵 → ∃𝑥 𝑥 = 𝐴)
4 exim 1490 . 2 (∀𝑥(𝑥 = 𝐴𝑥𝐵) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥 𝑥𝐵))
52, 3, 4sylc 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