Theorem elrabi 2970

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 2360	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)))
2		eleq1 2295	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
3	2	anbi1d 465	. . . . 5 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝑉 ∧ 𝜑) ↔ (𝐴 ∈ 𝑉 ∧ 𝜑)))
4	3	simprbda 383	. . . 4 ⊢ ((𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)) → 𝐴 ∈ 𝑉)
5	4	exlimiv 1647	. . 3 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)) → 𝐴 ∈ 𝑉)
6	1, 5	sylbi 121	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
7		df-rab 2529	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
8	6, 7	eleq2s 2327	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398  ∃wex 1541   ∈ wcel 2203  {cab 2218  {crab 2524

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-rab 2529

This theorem is referenced by:  rabsnif  3758  ordtriexmidlem  4641  ordtri2or2exmidlem  4648  onsucelsucexmidlem  4651  ordsoexmid  4684  reg3exmidlemwe  4701  elfvmptrab1  5772  acexmidlemcase  6045  elovmporab  6254  elovmporab1w  6255  ssfirab  7197  exmidonfinlem  7496  cc4f  7583  genpelvl  7827  genpelvu  7828  suplocsrlempr  8122  nnindnn  8208  sup3exmid  9231  nnind  9253  supinfneg  9927  infsupneg  9928  supminfex  9929  ublbneg  9945  zsupcllemstep  10589  infssuzex  10593  infssuzledc  10594  hashinfuni  11140  bezoutlemsup  12705  uzwodc  12733  nninfctlemfo  12736  lcmgcdlem  12774  phisum  12938  oddennn  13143  evenennn  13144  znnen  13149  ennnfonelemg  13154  rrgval  14407  psrbagf  14818  txdis1cn  15143  reopnap  15411  divcnap  15430  limccl  15524  dvlemap  15545  dvaddxxbr  15566  dvmulxxbr  15567  dvcoapbr  15572  dvcjbr  15573  dvrecap  15578  dveflem  15591  sgmval  15851  0sgm  15853  sgmf  15854  sgmnncl  15856  dvdsppwf1o  15857  sgmppw  15860  uhgrss  16070  usgredg2v  16219  subumgredg2en  16266  clwwlknon  16424