Theorem elex2 2819

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 2303	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
2	1	alrimiv 1922	. 2 ⊢ (𝐴 ∈ 𝐵 → ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
3		elisset 2817	. 2 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 = 𝐴)
4		exim 1647	. 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥 𝑥 ∈ 𝐵))
5	2, 3, 4	sylc 62	1 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵)

Syntax hints:   → wi 4  ∀wal 1395   = wceq 1397  ∃wex 1540   ∈ wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-v 2804

This theorem is referenced by:  snmg  3790  oprcl  3886  brm  4139  ss1o0el1  4287  exss  4319  onintrab2im  4616  regexmidlemm  4630  reldmm  4950  dmxpid  4953  acexmidlem2  6015  elmpom  6403  frecabcl  6565  ixpm  6899  en1m  6979  dom1o  7002  dom1oi  7003  enm  7004  ssfilem  7062  ssfilemd  7064  fin0  7074  fin0or  7075  diffitest  7076  diffisn  7082  infm  7096  inffiexmid  7098  ctssdc  7312  omct  7316  ctssexmid  7349  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  acnrcl  7416  exmidaclem  7423  iftrueb01  7441  pw1if  7443  caucvgsrlemasr  8010  suplocsrlempr  8027  gtso  8258  sup3exmid  9137  indstr  9827  negm  9849  fzm  10273  fzom  10400  rexfiuz  11554  r19.2uz  11558  resqrexlemgt0  11585  climuni  11858  bezoutlembi  12581  nninfct  12617  lcmgcdlem  12654  pcprecl  12867  pc2dvds  12908  4sqlem13m  12981  nninfdclemcl  13074  dfgrp3m  13687  issubg2m  13781  issubgrpd2  13782  issubg3  13784  issubg4m  13785  grpissubg  13786  subgintm  13790  nmzsubg  13802  ghmrn  13849  ghmpreima  13858  dvdsr02  14125  01eq0ring  14209  subrgugrp  14260  lmodfopnelem1  14344  rmodislmodlem  14370  rmodislmod  14371  lss1  14382  lsssubg  14397  islss3  14399  islss4  14402  lss1d  14403  lssintclm  14404  dflidl2rng  14501  lidlsubg  14506  cnsubglem  14599  tgioo  15284  elply2  15465  edgval  15917  wlkvtxm  16197  pw1nct  16630  nninfall  16637  nnnninfen  16649