Theorem elrabi 2956

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1395  ∃wex 1538   ∈ wcel 2200  {cab 2215  {crab 2512

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-rab 2517

This theorem is referenced by:  ordtriexmidlem  4611  ordtri2or2exmidlem  4618  onsucelsucexmidlem  4621  ordsoexmid  4654  reg3exmidlemwe  4671  elfvmptrab1  5731  acexmidlemcase  6002  elovmporab  6211  elovmporab1w  6212  ssfirab  7109  exmidonfinlem  7382  cc4f  7466  genpelvl  7710  genpelvu  7711  suplocsrlempr  8005  nnindnn  8091  sup3exmid  9115  nnind  9137  supinfneg  9802  infsupneg  9803  supminfex  9804  ublbneg  9820  zsupcllemstep  10461  infssuzex  10465  infssuzledc  10466  hashinfuni  11011  bezoutlemsup  12545  uzwodc  12573  nninfctlemfo  12576  lcmgcdlem  12614  phisum  12778  oddennn  12978  evenennn  12979  znnen  12984  ennnfonelemg  12989  rrgval  14241  psrbagf  14649  txdis1cn  14967  reopnap  15235  divcnap  15254  limccl  15348  dvlemap  15369  dvaddxxbr  15390  dvmulxxbr  15391  dvcoapbr  15396  dvcjbr  15397  dvrecap  15402  dveflem  15415  sgmval  15672  0sgm  15674  sgmf  15675  sgmnncl  15677  dvdsppwf1o  15678  sgmppw  15681  uhgrss  15890  usgredg2v  16037