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

Theorem elex2 2657
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 2171 . . 3 (𝐴𝐵 → (𝑥 = 𝐴𝑥𝐵))
21alrimiv 1813 . 2 (𝐴𝐵 → ∀𝑥(𝑥 = 𝐴𝑥𝐵))
3 elisset 2655 . 2 (𝐴𝐵 → ∃𝑥 𝑥 = 𝐴)
4 exim 1546 . 2 (∀𝑥(𝑥 = 𝐴𝑥𝐵) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥 𝑥𝐵))
52, 3, 4sylc 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