Theorem elex2 2737

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

Step	Hyp	Ref	Expression
1		eleq1a 2236	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
2	1	alrimiv 1861	. 2 ⊢ (𝐴 ∈ 𝐵 → ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
3		elisset 2735	. 2 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 = 𝐴)
4		exim 1586	. 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥 𝑥 ∈ 𝐵))
5	2, 3, 4	sylc 62	1 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵)

Syntax hints:   → wi 4  ∀wal 1340   = wceq 1342  ∃wex 1479   ∈ wcel 2135

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 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-v 2723

This theorem is referenced by:  snmg  3688  oprcl  3776  brm  4026  ss1o0el1  4170  exss  4199  onintrab2im  4489  regexmidlemm  4503  dmxpid  4819  acexmidlem2  5833  frecabcl  6358  ixpm  6687  enm  6777  ssfilem  6832  fin0  6842  fin0or  6843  diffitest  6844  diffisn  6850  infm  6861  inffiexmid  6863  ctssdc  7069  omct  7073  ctssexmid  7105  exmidfodomrlemr  7149  exmidfodomrlemrALT  7150  exmidaclem  7155  caucvgsrlemasr  7722  suplocsrlempr  7739  gtso  7968  sup3exmid  8843  indstr  9522  negm  9544  fzm  9963  fzom  10089  rexfiuz  10917  r19.2uz  10921  resqrexlemgt0  10948  climuni  11220  bezoutlembi  11923  lcmgcdlem  11988  pcprecl  12198  pc2dvds  12238  nninfdclemcl  12320  tgioo  13087  pw1nct  13717  nninfall  13723