Theorem elrabi 3328

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 2735	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)))
2		eleq1 2676	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
3	2	anbi1d 737	. . . . 5 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝑉 ∧ 𝜑) ↔ (𝐴 ∈ 𝑉 ∧ 𝜑)))
4	3	simprbda 651	. . . 4 ⊢ ((𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)) → 𝐴 ∈ 𝑉)
5	4	exlimiv 1845	. . 3 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)) → 𝐴 ∈ 𝑉)
6	1, 5	sylbi 206	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
7		df-rab 2905	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
8	6, 7	eleq2s 2706	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475  ∃wex 1695   ∈ wcel 1977  {cab 2596  {crab 2900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-rab 2905

This theorem is referenced by:  elfvmptrab1  6213  elovmpt2rab  6778  elovmpt2rab1  6779  elovmpt3rab1  6791  mapfienlem1  8193  mapfienlem2  8194  mapfienlem3  8195  kmlem1  8855  fin1a2lem9  9113  nnind  10915  ublbneg  11649  supminf  11651  rlimrege0  14158  incexc2  14409  lcmgcdlem  15157  phisum  15333  prmgaplem5  15597  isinitoi  16476  istermoi  16477  odcl  17778  odlem2  17781  gexcl  17818  gexlem2  17820  gexdvds  17822  pgpssslw  17852  resspsrmul  19238  mplbas2  19291  mptcoe1fsupp  19406  psropprmul  19429  coe1mul2  19460  psgnfix2  19764  psgndiflemB  19765  psgndif  19767  zrhcopsgndif  19768  cpmatpmat  20334  mptcoe1matfsupp  20426  mp2pm2mplem4  20433  chpscmat  20466  chpscmatgsumbin  20468  chpscmatgsummon  20469  txdis1cn  21248  ptcmplem3  21668  rrxmvallem  22995  mdegmullem  23642  0sgm  24670  sgmf  24671  sgmnncl  24673  fsumdvdsdiaglem  24709  fsumdvdscom  24711  dvdsppwf1o  24712  dvdsflf1o  24713  musumsum  24718  muinv  24719  sgmppw  24722  rpvmasumlem  24976  dchrmusum2  24983  dchrvmasumlem1  24984  dchrvmasum2lem  24985  dchrisum0fmul  24995  dchrisum0ff  24996  dchrisum0flblem1  24997  dchrisum0  25009  logsqvma  25031  usgraidx2v  25922  uvtxisvtx  26018  clwlkf1clwwlk  26377  2wlkonot3v  26402  2spthonot3v  26403  rusgranumwlks  26483  frgrawopreglem4  26574  frgrawopreg  26576  numclwwlkun  26606  rabsnel  28726  nnindf  28952  ddemeas  29626  imambfm  29651  eulerpartlemgs2  29769  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemirc  29920  bnj110  30182  poimirlem4  32583  poimirlem5  32584  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem9  32588  poimirlem10  32589  poimirlem11  32590  poimirlem12  32591  poimirlem13  32592  poimirlem14  32593  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem18  32597  poimirlem19  32598  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem26  32605  mblfinlem2  32617  rencldnfilem  36402  irrapx1  36410  radcnvrat  37535  fsumiunss  38642  dvnprodlem1  38836  stoweidlem15  38908  stoweidlem31  38924  fourierdlem25  39025  fourierdlem51  39050  fourierdlem79  39078  etransclem28  39155  issalgend  39232  sge0iunmptlemre  39308  hoidmvlelem2  39486  issmflem  39613  smfresal  39673  usgredg2v  40454  umgrres1lem  40529  upgrres1  40532  uvtxaisvtx  40615  rusgrnumwwlks  41177  clwlksf1clwwlk  41276  frgrwopreglem4  41484  frgrwopreg  41486  2zrngasgrp  41730  2zrngamnd  41731  2zrngacmnd  41732  2zrngagrp  41733  2zrngmsgrp  41737  2zrngALT  41738  2zrngnmlid  41739  2zrngnmlid2  41741