Theorem elex2 2755

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 2249	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
2	1	alrimiv 1874	. 2 ⊢ (𝐴 ∈ 𝐵 → ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
3		elisset 2753	. 2 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 = 𝐴)
4		exim 1599	. 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥 𝑥 ∈ 𝐵))
5	2, 3, 4	sylc 62	1 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵)

Syntax hints:   → wi 4  ∀wal 1351   = wceq 1353  ∃wex 1492   ∈ wcel 2148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-v 2741

This theorem is referenced by:  snmg  3712  oprcl  3804  brm  4055  ss1o0el1  4199  exss  4229  onintrab2im  4519  regexmidlemm  4533  dmxpid  4850  acexmidlem2  5874  frecabcl  6402  ixpm  6732  enm  6822  ssfilem  6877  fin0  6887  fin0or  6888  diffitest  6889  diffisn  6895  infm  6906  inffiexmid  6908  ctssdc  7114  omct  7118  ctssexmid  7150  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  exmidaclem  7209  caucvgsrlemasr  7791  suplocsrlempr  7808  gtso  8038  sup3exmid  8916  indstr  9595  negm  9617  fzm  10040  fzom  10166  rexfiuz  11000  r19.2uz  11004  resqrexlemgt0  11031  climuni  11303  bezoutlembi  12008  lcmgcdlem  12079  pcprecl  12291  pc2dvds  12331  nninfdclemcl  12451  dfgrp3m  12974  issubg2m  13054  issubgrpd2  13055  issubg3  13057  issubg4m  13058  grpissubg  13059  subgintm  13063  nmzsubg  13075  dvdsr02  13279  01eq0ring  13335  subrgugrp  13366  lmodfopnelem1  13419  rmodislmodlem  13445  rmodislmod  13446  lss1  13454  lsssubg  13469  islss3  13471  islss4  13474  lss1d  13475  lssintclm  13476  cnsubglem  13512  tgioo  14085  pw1nct  14791  nninfall  14797