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  4668  ordtri2or2exmidlem  4675  onsucelsucexmidlem  4678  ordsoexmid  4711  reg3exmidlemwe  4728  elfvmptrab1  5804  acexmidlemcase  6083  elovmporab  6292  elovmporab1w  6293  ssfirab  7248  exmidonfinlem  7551  cc4f  7641  genpelvl  7885  genpelvu  7886  suplocsrlempr  8180  nnindnn  8266  sup3exmid  9295  nnind  9329  supinfneg  10011  infsupneg  10012  supminfex  10013  ublbneg  10029  zsupcllemstep  10679  infssuzex  10683  infssuzledc  10684  hashinfuni  11238  bezoutlemsup  12811  uzwodc  12839  nninfctlemfo  12842  lcmgcdlem  12880  phisum  13048  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemfrcn0  13331  ballotfilemirc  13333  oddennn  13341  evenennn  13342  znnen  13347  ennnfonelemg  13352  cntzval  14153  rrgval  14679  psrbagf  15163  gsumbagdiagfi  15176  rhmpsrfilem2  15185  psrmulvalfi  15188  txdis1cn  15504  reopnap  15772  divcnap  15791  limccl  15885  dvlemap  15906  dvaddxxbr  15927  dvmulxxbr  15928  dvcoapbr  15933  dvcjbr  15934  dvrecap  15939  dveflem  15952  sgmval  16252  0sgm  16254  sgmf  16255  sgmnncl  16257  dvdsppwf1o  16283  sgmppw  16286  uhgrss  16521  usgredg2v  16670  subumgredg2en  16717  clwwlknon  16875