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 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   = wceq 1402  ∃wex 1545   ∈ wcel 2209  {cab 2224  {crab 2532

This proof depends on 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 proof 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 used by:  rabsnif  3778  ordtriexmidlem  4666  ordtri2or2exmidlem  4673  onsucelsucexmidlem  4676  ordsoexmid  4709  reg3exmidlemwe  4726  elfvmptrab1  5801  acexmidlemcase  6080  elovmporab  6289  elovmporab1w  6290  ssfirab  7244  exmidonfinlem  7545  cc4f  7635  genpelvl  7879  genpelvu  7880  suplocsrlempr  8174  nnindnn  8260  sup3exmid  9289  nnind  9322  supinfneg  10004  infsupneg  10005  supminfex  10006  ublbneg  10022  zsupcllemstep  10672  infssuzex  10676  infssuzledc  10677  hashinfuni  11230  bezoutlemsup  12802  uzwodc  12830  nninfctlemfo  12833  lcmgcdlem  12871  phisum  13039  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemfrcn0  13322  ballotfilemirc  13324  oddennn  13332  evenennn  13333  znnen  13338  ennnfonelemg  13343  rrgval  14619  psrbagf  15103  txdis1cn  15428  reopnap  15696  divcnap  15715  limccl  15809  dvlemap  15830  dvaddxxbr  15851  dvmulxxbr  15852  dvcoapbr  15857  dvcjbr  15858  dvrecap  15863  dveflem  15876  sgmval  16164  0sgm  16166  sgmf  16167  sgmnncl  16169  dvdsppwf1o  16184  sgmppw  16187  uhgrss  16414  usgredg2v  16563  subumgredg2en  16610  clwwlknon  16768