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

Theorem elex2 2705
 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 2212 . . 3 (𝐴𝐵 → (𝑥 = 𝐴𝑥𝐵))
21alrimiv 1847 . 2 (𝐴𝐵 → ∀𝑥(𝑥 = 𝐴𝑥𝐵))
3 elisset 2703 . 2 (𝐴𝐵 → ∃𝑥 𝑥 = 𝐴)
4 exim 1579 . 2 (∀𝑥(𝑥 = 𝐴𝑥𝐵) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥 𝑥𝐵))
52, 3, 4sylc 62 1 (𝐴𝐵 → ∃𝑥 𝑥𝐵)
 Colors of variables: wff set class Syntax hints:   → wi 4  ∀wal 1330   = wceq 1332  ∃wex 1469   ∈ wcel 1481 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-v 2691 This theorem is referenced by:  snmg  3648  oprcl  3736  brm  3985  exmid01  4128  exss  4156  onintrab2im  4441  regexmidlemm  4454  dmxpid  4767  acexmidlem2  5778  frecabcl  6303  ixpm  6631  enm  6721  ssfilem  6776  fin0  6786  fin0or  6787  diffitest  6788  diffisn  6794  infm  6805  inffiexmid  6807  ctssdc  7005  omct  7009  ctssexmid  7031  exmidfodomrlemr  7074  exmidfodomrlemrALT  7075  exmidaclem  7080  caucvgsrlemasr  7621  suplocsrlempr  7638  gtso  7866  sup3exmid  8738  indstr  9414  negm  9433  fzm  9848  fzom  9971  rexfiuz  10792  r19.2uz  10796  resqrexlemgt0  10823  climuni  11093  bezoutlembi  11727  lcmgcdlem  11792  tgioo  12752  pw1nct  13369  nninfall  13377
 Copyright terms: Public domain W3C validator