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  4610  ordtri2or2exmidlem  4617  onsucelsucexmidlem  4620  ordsoexmid  4653  reg3exmidlemwe  4670  elfvmptrab1  5728  acexmidlemcase  5995  elovmporab  6204  elovmporab1w  6205  ssfirab  7094  exmidonfinlem  7367  cc4f  7451  genpelvl  7695  genpelvu  7696  suplocsrlempr  7990  nnindnn  8076  sup3exmid  9100  nnind  9122  supinfneg  9786  infsupneg  9787  supminfex  9788  ublbneg  9804  zsupcllemstep  10444  infssuzex  10448  infssuzledc  10449  hashinfuni  10994  bezoutlemsup  12525  uzwodc  12553  nninfctlemfo  12556  lcmgcdlem  12594  phisum  12758  oddennn  12958  evenennn  12959  znnen  12964  ennnfonelemg  12969  rrgval  14220  psrbagf  14628  txdis1cn  14946  reopnap  15214  divcnap  15233  limccl  15327  dvlemap  15348  dvaddxxbr  15369  dvmulxxbr  15370  dvcoapbr  15375  dvcjbr  15376  dvrecap  15381  dveflem  15394  sgmval  15651  0sgm  15653  sgmf  15654  sgmnncl  15656  dvdsppwf1o  15657  sgmppw  15660  uhgrss  15869  usgredg2v  16016