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

Theorem elex2 2676
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 2189 . . 3 (𝐴𝐵 → (𝑥 = 𝐴𝑥𝐵))
21alrimiv 1830 . 2 (𝐴𝐵 → ∀𝑥(𝑥 = 𝐴𝑥𝐵))
3 elisset 2674 . 2 (𝐴𝐵 → ∃𝑥 𝑥 = 𝐴)
4 exim 1563 . 2 (∀𝑥(𝑥 = 𝐴𝑥𝐵) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥 𝑥𝐵))
52, 3, 4sylc 62 1 (𝐴𝐵 → ∃𝑥 𝑥𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1314   = wceq 1316  wex 1453  wcel 1465
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 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-v 2662
This theorem is referenced by:  snmg  3611  oprcl  3699  brm  3948  exmid01  4091  exss  4119  onintrab2im  4404  regexmidlemm  4417  dmxpid  4730  acexmidlem2  5739  frecabcl  6264  ixpm  6592  enm  6682  ssfilem  6737  fin0  6747  fin0or  6748  diffitest  6749  diffisn  6755  infm  6766  inffiexmid  6768  ctssdc  6966  omct  6970  ctssexmid  6992  exmidfodomrlemr  7026  exmidfodomrlemrALT  7027  exmidaclem  7032  caucvgsrlemasr  7566  suplocsrlempr  7583  gtso  7811  sup3exmid  8683  indstr  9356  negm  9375  fzm  9786  fzom  9909  rexfiuz  10729  r19.2uz  10733  resqrexlemgt0  10760  climuni  11030  bezoutlembi  11620  lcmgcdlem  11685  tgioo  12642  nninfall  13131
  Copyright terms: Public domain W3C validator