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  9287  nnind  9320  supinfneg  9995  infsupneg  9996  supminfex  9997  ublbneg  10013  zsupcllemstep  10662  infssuzex  10666  infssuzledc  10667  hashinfuni  11216  bezoutlemsup  12786  uzwodc  12814  nninfctlemfo  12817  lcmgcdlem  12855  phisum  13019  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemfrcn0  13273  ballotfilemirc  13275  oddennn  13283  evenennn  13284  znnen  13289  ennnfonelemg  13294  rrgval  14570  psrbagf  15054  txdis1cn  15379  reopnap  15647  divcnap  15666  limccl  15760  dvlemap  15781  dvaddxxbr  15802  dvmulxxbr  15803  dvcoapbr  15808  dvcjbr  15809  dvrecap  15814  dveflem  15827  sgmval  16097  0sgm  16099  sgmf  16100  sgmnncl  16102  dvdsppwf1o  16103  sgmppw  16106  uhgrss  16316  usgredg2v  16465  subumgredg2en  16512  clwwlknon  16670