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  7250  exmidonfinlem  7551  cc4f  7641  genpelvl  7885  genpelvu  7886  suplocsrlempr  8180  nnindnn  8266  sup3exmid  9295  nnind  9329  supinfneg  10010  infsupneg  10011  supminfex  10012  ublbneg  10028  zsupcllemstep  10678  infssuzex  10682  infssuzledc  10683  hashinfuni  11237  bezoutlemsup  12810  uzwodc  12838  nninfctlemfo  12841  lcmgcdlem  12879  phisum  13047  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemfrcn0  13330  ballotfilemirc  13332  oddennn  13340  evenennn  13341  znnen  13346  ennnfonelemg  13351  cntzval  14152  rrgval  14678  psrbagf  15164  gsumbagdiagfi  15185  rhmpsrfilem2  15194  psrmulvalfi  15197  mplbas  15223  txdis1cn  15521  reopnap  15789  divcnap  15808  limccl  15902  dvlemap  15923  dvaddxxbr  15944  dvmulxxbr  15945  dvcoapbr  15950  dvcjbr  15951  dvrecap  15956  dveflem  15969  sgmval  16269  0sgm  16271  sgmf  16272  sgmnncl  16274  dvdsppwf1o  16300  sgmppw  16303  uhgrss  16538  usgredg2v  16687  subumgredg2en  16734  clwwlknon  16892