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

Theorem elex2 2616
 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 2151 . . 3 (𝐴𝐵 → (𝑥 = 𝐴𝑥𝐵))
21alrimiv 1796 . 2 (𝐴𝐵 → ∀𝑥(𝑥 = 𝐴𝑥𝐵))
3 elisset 2614 . 2 (𝐴𝐵 → ∃𝑥 𝑥 = 𝐴)
4 exim 1531 . 2 (∀𝑥(𝑥 = 𝐴𝑥𝐵) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥 𝑥𝐵))
52, 3, 4sylc 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