Theorem elrabi 3359

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 2748	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)))
2		eleq1 2689	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
3	2	anbi1d 741	. . . . 5 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝑉 ∧ 𝜑) ↔ (𝐴 ∈ 𝑉 ∧ 𝜑)))
4	3	simprbda 653	. . . 4 ⊢ ((𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)) → 𝐴 ∈ 𝑉)
5	4	exlimiv 1858	. . 3 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)) → 𝐴 ∈ 𝑉)
6	1, 5	sylbi 207	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
7		df-rab 2921	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
8	6, 7	eleq2s 2719	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1483  ∃wex 1704   ∈ wcel 1990  {cab 2608  {crab 2916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-rab 2921

This theorem is referenced by:  elfvmptrab1  6305  elovmpt2rab  6880  elovmpt2rab1  6881  elovmpt3rab1  6893  mapfienlem1  8310  mapfienlem2  8311  mapfienlem3  8312  kmlem1  8972  fin1a2lem9  9230  nnind  11038  ublbneg  11773  supminf  11775  rlimrege0  14310  incexc2  14570  lcmgcdlem  15319  phisum  15495  prmgaplem5  15759  isinitoi  16653  istermoi  16654  odcl  17955  odlem2  17958  gexcl  17995  gexlem2  17997  gexdvds  17999  pgpssslw  18029  resspsrmul  19417  mplbas2  19470  mptcoe1fsupp  19585  psropprmul  19608  coe1mul2  19639  psgnfix2  19945  psgndiflemB  19946  psgndif  19948  zrhcopsgndif  19949  cpmatpmat  20515  mptcoe1matfsupp  20607  mp2pm2mplem4  20614  chpscmat  20647  chpscmatgsumbin  20649  chpscmatgsummon  20650  txdis1cn  21438  ptcmplem3  21858  rrxmvallem  23187  mdegmullem  23838  0sgm  24870  sgmf  24871  sgmnncl  24873  fsumdvdsdiaglem  24909  fsumdvdscom  24911  dvdsppwf1o  24912  dvdsflf1o  24913  musumsum  24918  muinv  24919  sgmppw  24922  rpvmasumlem  25176  dchrmusum2  25183  dchrvmasumlem1  25184  dchrvmasum2lem  25185  dchrisum0fmul  25195  dchrisum0ff  25196  dchrisum0flblem1  25197  dchrisum0  25209  logsqvma  25231  usgredg2v  26119  umgrres1lem  26202  upgrres1  26205  uvtxaisvtx  26289  vtxdgoddnumeven  26449  rusgrnumwwlks  26869  clwlksf1clwwlk  26969  frgrwopreglem4  27179  frgrwopreg  27187  rabsnel  29341  nnindf  29565  ddemeas  30299  imambfm  30324  eulerpartlemgs2  30442  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemirc  30593  reprf  30690  tgoldbachgnn  30737  tgoldbachgt  30741  bnj110  30928  poimirlem4  33413  poimirlem5  33414  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem9  33418  poimirlem10  33419  poimirlem11  33420  poimirlem12  33421  poimirlem13  33422  poimirlem14  33423  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem18  33427  poimirlem19  33428  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem26  33435  mblfinlem2  33447  rencldnfilem  37384  irrapx1  37392  radcnvrat  38513  supminfxr  39694  fsumiunss  39807  dvnprodlem1  40161  stoweidlem15  40232  stoweidlem31  40248  fourierdlem25  40349  fourierdlem51  40374  fourierdlem79  40402  etransclem28  40479  issalgend  40556  sge0iunmptlemre  40632  hoidmvlelem2  40810  issmflem  40936  smfresal  40995  2zrngasgrp  41940  2zrngamnd  41941  2zrngacmnd  41942  2zrngagrp  41943  2zrngmsgrp  41947  2zrngALT  41948  2zrngnmlid  41949  2zrngnmlid2  41951