Theorem elrabi 3623

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 2933	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)))
2		eleq1 2877	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
3	2	anbi1d 632	. . . . 5 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝑉 ∧ 𝜑) ↔ (𝐴 ∈ 𝑉 ∧ 𝜑)))
4	3	simprbda 502	. . . 4 ⊢ ((𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)) → 𝐴 ∈ 𝑉)
5	4	exlimiv 1931	. . 3 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)) → 𝐴 ∈ 𝑉)
6	1, 5	sylbi 220	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
7		df-rab 3115	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
8	6, 7	eleq2s 2908	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  {cab 2776  {crab 3110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115

This theorem is referenced by:  elfvmptrab1w  6771  elfvmptrab1  6772  elovmporab  7371  elovmporab1w  7372  elovmporab1  7373  elovmpt3rab1  7385  mapfienlem1  8852  mapfienlem2  8853  mapfienlem3  8854  kmlem1  9561  fin1a2lem9  9819  nnind  11643  ublbneg  12321  supminf  12323  rlimrege0  14928  incexc2  15185  lcmgcdlem  15940  phisum  16117  prmgaplem5  16381  isinitoi  17255  istermoi  17256  odcl  18656  odlem2  18659  gexcl  18697  gexlem2  18699  gexdvds  18701  pgpssslw  18731  psgnfix2  20288  psgndiflemB  20289  psgndif  20291  copsgndif  20292  resspsrmul  20655  mplbas2  20710  mptcoe1fsupp  20844  psropprmul  20867  coe1mul2  20898  cpmatpmat  21315  mptcoe1matfsupp  21407  mp2pm2mplem4  21414  chpscmat  21447  chpscmatgsumbin  21449  chpscmatgsummon  21450  txdis1cn  22240  ptcmplem3  22659  rrxmvallem  24008  mdegmullem  24679  0sgm  25729  sgmf  25730  sgmnncl  25732  fsumdvdsdiaglem  25768  fsumdvdscom  25770  dvdsppwf1o  25771  dvdsflf1o  25772  musumsum  25777  muinv  25778  sgmppw  25781  rpvmasumlem  26071  dchrmusum2  26078  dchrvmasumlem1  26079  dchrvmasum2lem  26080  dchrisum0fmul  26090  dchrisum0ff  26091  dchrisum0flblem1  26092  dchrisum0  26104  logsqvma  26126  usgredg2v  27017  umgrres1lem  27100  upgrres1  27103  vtxdgoddnumeven  27343  rusgrnumwwlks  27760  frgrwopreglem4  28100  frgrwopreg  28108  rabsnel  30270  nnindf  30561  cyc3evpm  30842  cycpmgcl  30845  cycpmconjslem2  30847  ddemeas  31605  imambfm  31630  eulerpartlemgs2  31748  ballotlemfc0  31860  ballotlemfcc  31861  ballotlemirc  31899  reprf  31993  tgoldbachgnn  32040  tgoldbachgt  32044  bnj110  32240  fnrelpredd  32472  poimirlem4  35061  poimirlem5  35062  poimirlem6  35063  poimirlem7  35064  poimirlem8  35065  poimirlem9  35066  poimirlem10  35067  poimirlem11  35068  poimirlem12  35069  poimirlem13  35070  poimirlem14  35071  poimirlem15  35072  poimirlem16  35073  poimirlem17  35074  poimirlem18  35075  poimirlem19  35076  poimirlem20  35077  poimirlem21  35078  poimirlem22  35079  poimirlem26  35083  mblfinlem2  35095  rencldnfilem  39761  irrapx1  39769  scottelrankd  40955  radcnvrat  41018  supminfxr  42103  fsumiunss  42217  dvnprodlem1  42588  stoweidlem15  42657  stoweidlem31  42673  fourierdlem25  42774  fourierdlem51  42799  fourierdlem79  42827  etransclem28  42904  issalgend  42978  sge0iunmptlemre  43054  hoidmvlelem2  43235  issmflem  43361  smfresal  43420  2zrngasgrp  44564  2zrngamnd  44565  2zrngacmnd  44566  2zrngagrp  44567  2zrngmsgrp  44571  2zrngALT  44572  2zrngnmlid  44573  2zrngnmlid2  44575