Theorem elrabi 2925

Description: Implication for the membership in a restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017.)

Assertion

Ref	Expression
elrabi	⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Distinct variable groups:   𝑥,𝐴   𝑥,𝑉

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem elrabi

Step	Hyp	Ref	Expression
1		clelab 2330	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)))
2		eleq1 2267	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
3	2	anbi1d 465	. . . . 5 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝑉 ∧ 𝜑) ↔ (𝐴 ∈ 𝑉 ∧ 𝜑)))
4	3	simprbda 383	. . . 4 ⊢ ((𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)) → 𝐴 ∈ 𝑉)
5	4	exlimiv 1620	. . 3 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)) → 𝐴 ∈ 𝑉)
6	1, 5	sylbi 121	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
7		df-rab 2492	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
8	6, 7	eleq2s 2299	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1372  ∃wex 1514   ∈ wcel 2175  {cab 2190  {crab 2487

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-rab 2492

This theorem is referenced by:  ordtriexmidlem  4566  ordtri2or2exmidlem  4573  onsucelsucexmidlem  4576  ordsoexmid  4609  reg3exmidlemwe  4626  elfvmptrab1  5673  acexmidlemcase  5938  elovmporab  6145  elovmporab1w  6146  ssfirab  7032  exmidonfinlem  7300  cc4f  7380  genpelvl  7624  genpelvu  7625  suplocsrlempr  7919  nnindnn  8005  sup3exmid  9029  nnind  9051  supinfneg  9715  infsupneg  9716  supminfex  9717  ublbneg  9733  zsupcllemstep  10370  infssuzex  10374  infssuzledc  10375  hashinfuni  10920  bezoutlemsup  12301  uzwodc  12329  nninfctlemfo  12332  lcmgcdlem  12370  phisum  12534  oddennn  12734  evenennn  12735  znnen  12740  ennnfonelemg  12745  rrgval  13995  psrbagf  14403  txdis1cn  14721  reopnap  14989  divcnap  15008  limccl  15102  dvlemap  15123  dvaddxxbr  15144  dvmulxxbr  15145  dvcoapbr  15150  dvcjbr  15151  dvrecap  15156  dveflem  15169  sgmval  15426  0sgm  15428  sgmf  15429  sgmnncl  15431  dvdsppwf1o  15432  sgmppw  15435