Theorem elrabi 2979

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 2366	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)))
2		eleq1 2301	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
3	2	anbi1d 469	. . . . 5 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝑉 ∧ 𝜑) ↔ (𝐴 ∈ 𝑉 ∧ 𝜑)))
4	3	simprbda 383	. . . 4 ⊢ ((𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)) → 𝐴 ∈ 𝑉)
5	4	exlimiv 1651	. . 3 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)) → 𝐴 ∈ 𝑉)
6	1, 5	sylbi 121	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
7		df-rab 2537	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
8	6, 7	eleq2s 2333	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1402  ∃wex 1545   ∈ wcel 2209  {cab 2224  {crab 2532

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-rab 2537

This theorem is referenced by:  rabsnif  3774  ordtriexmidlem  4661  ordtri2or2exmidlem  4668  onsucelsucexmidlem  4671  ordsoexmid  4704  reg3exmidlemwe  4721  elfvmptrab1  5794  acexmidlemcase  6070  elovmporab  6279  elovmporab1w  6280  ssfirab  7234  exmidonfinlem  7535  cc4f  7625  genpelvl  7869  genpelvu  7870  suplocsrlempr  8164  nnindnn  8250  sup3exmid  9277  nnind  9299  supinfneg  9974  infsupneg  9975  supminfex  9976  ublbneg  9992  zsupcllemstep  10640  infssuzex  10644  infssuzledc  10645  hashinfuni  11194  bezoutlemsup  12764  uzwodc  12792  nninfctlemfo  12795  lcmgcdlem  12833  phisum  12997  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemfrcn0  13251  ballotfilemirc  13253  oddennn  13261  evenennn  13262  znnen  13267  ennnfonelemg  13272  rrgval  14543  psrbagf  14977  txdis1cn  15302  reopnap  15570  divcnap  15589  limccl  15683  dvlemap  15704  dvaddxxbr  15725  dvmulxxbr  15726  dvcoapbr  15731  dvcjbr  15732  dvrecap  15737  dveflem  15750  sgmval  16011  0sgm  16013  sgmf  16014  sgmnncl  16016  dvdsppwf1o  16017  sgmppw  16020  uhgrss  16230  usgredg2v  16379  subumgredg2en  16426  clwwlknon  16584