Theorem elrabi 3677

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 2960	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)))
2		eleq1 2902	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
3	2	anbi1d 631	. . . . 5 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝑉 ∧ 𝜑) ↔ (𝐴 ∈ 𝑉 ∧ 𝜑)))
4	3	simprbda 501	. . . 4 ⊢ ((𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)) → 𝐴 ∈ 𝑉)
5	4	exlimiv 1931	. . 3 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)) → 𝐴 ∈ 𝑉)
6	1, 5	sylbi 219	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
7		df-rab 3149	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
8	6, 7	eleq2s 2933	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537  ∃wex 1780   ∈ wcel 2114  {cab 2801  {crab 3144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-rab 3149

This theorem is referenced by:  elfvmptrab1w  6796  elfvmptrab1  6797  elovmporab  7393  elovmporab1w  7394  elovmporab1  7395  elovmpt3rab1  7407  mapfienlem1  8870  mapfienlem2  8871  mapfienlem3  8872  kmlem1  9578  fin1a2lem9  9832  nnind  11658  ublbneg  12336  supminf  12338  rlimrege0  14938  incexc2  15195  lcmgcdlem  15952  phisum  16129  prmgaplem5  16393  isinitoi  17265  istermoi  17266  odcl  18666  odlem2  18669  gexcl  18707  gexlem2  18709  gexdvds  18711  pgpssslw  18741  resspsrmul  20199  mplbas2  20253  mptcoe1fsupp  20385  psropprmul  20408  coe1mul2  20439  psgnfix2  20745  psgndiflemB  20746  psgndif  20748  copsgndif  20749  cpmatpmat  21320  mptcoe1matfsupp  21412  mp2pm2mplem4  21419  chpscmat  21452  chpscmatgsumbin  21454  chpscmatgsummon  21455  txdis1cn  22245  ptcmplem3  22664  rrxmvallem  24009  mdegmullem  24674  0sgm  25723  sgmf  25724  sgmnncl  25726  fsumdvdsdiaglem  25762  fsumdvdscom  25764  dvdsppwf1o  25765  dvdsflf1o  25766  musumsum  25771  muinv  25772  sgmppw  25775  rpvmasumlem  26065  dchrmusum2  26072  dchrvmasumlem1  26073  dchrvmasum2lem  26074  dchrisum0fmul  26084  dchrisum0ff  26085  dchrisum0flblem1  26086  dchrisum0  26098  logsqvma  26120  usgredg2v  27011  umgrres1lem  27094  upgrres1  27097  vtxdgoddnumeven  27337  rusgrnumwwlks  27755  frgrwopreglem4  28096  frgrwopreg  28104  rabsnel  30265  nnindf  30537  cyc3evpm  30794  cycpmgcl  30797  cycpmconjslem2  30799  ddemeas  31497  imambfm  31522  eulerpartlemgs2  31640  ballotlemfc0  31752  ballotlemfcc  31753  ballotlemirc  31791  reprf  31885  tgoldbachgnn  31932  tgoldbachgt  31936  bnj110  32132  poimirlem4  34898  poimirlem5  34899  poimirlem6  34900  poimirlem7  34901  poimirlem8  34902  poimirlem9  34903  poimirlem10  34904  poimirlem11  34905  poimirlem12  34906  poimirlem13  34907  poimirlem14  34908  poimirlem15  34909  poimirlem16  34910  poimirlem17  34911  poimirlem18  34912  poimirlem19  34913  poimirlem20  34914  poimirlem21  34915  poimirlem22  34916  poimirlem26  34920  mblfinlem2  34932  rencldnfilem  39424  irrapx1  39432  scottelrankd  40590  radcnvrat  40653  supminfxr  41747  fsumiunss  41863  dvnprodlem1  42238  stoweidlem15  42307  stoweidlem31  42323  fourierdlem25  42424  fourierdlem51  42449  fourierdlem79  42477  etransclem28  42554  issalgend  42628  sge0iunmptlemre  42704  hoidmvlelem2  42885  issmflem  43011  smfresal  43070  2zrngasgrp  44218  2zrngamnd  44219  2zrngacmnd  44220  2zrngagrp  44221  2zrngmsgrp  44225  2zrngALT  44226  2zrngnmlid  44227  2zrngnmlid2  44229