Theorem elrabi 2960

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 2358	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)))
2		eleq1 2294	. . . . . 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 2520	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
8	6, 7	eleq2s 2326	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398  ∃wex 1541   ∈ wcel 2202  {cab 2217  {crab 2515

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 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-rab 2520

This theorem is referenced by:  rabsnif  3742  ordtriexmidlem  4623  ordtri2or2exmidlem  4630  onsucelsucexmidlem  4633  ordsoexmid  4666  reg3exmidlemwe  4683  elfvmptrab1  5750  acexmidlemcase  6023  elovmporab  6232  elovmporab1w  6233  ssfirab  7172  exmidonfinlem  7447  cc4f  7531  genpelvl  7775  genpelvu  7776  suplocsrlempr  8070  nnindnn  8156  sup3exmid  9179  nnind  9201  supinfneg  9873  infsupneg  9874  supminfex  9875  ublbneg  9891  zsupcllemstep  10535  infssuzex  10539  infssuzledc  10540  hashinfuni  11085  bezoutlemsup  12643  uzwodc  12671  nninfctlemfo  12674  lcmgcdlem  12712  phisum  12876  oddennn  13076  evenennn  13077  znnen  13082  ennnfonelemg  13087  rrgval  14340  psrbagf  14749  txdis1cn  15072  reopnap  15340  divcnap  15359  limccl  15453  dvlemap  15474  dvaddxxbr  15495  dvmulxxbr  15496  dvcoapbr  15501  dvcjbr  15502  dvrecap  15507  dveflem  15520  sgmval  15780  0sgm  15782  sgmf  15783  sgmnncl  15785  dvdsppwf1o  15786  sgmppw  15789  uhgrss  15999  usgredg2v  16148  subumgredg2en  16195  clwwlknon  16353