Theorem elrabi 3567

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 2916	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)))
2		eleq1 2847	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
3	2	anbi1d 623	. . . . 5 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝑉 ∧ 𝜑) ↔ (𝐴 ∈ 𝑉 ∧ 𝜑)))
4	3	simprbda 494	. . . 4 ⊢ ((𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)) → 𝐴 ∈ 𝑉)
5	4	exlimiv 1973	. . 3 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)) → 𝐴 ∈ 𝑉)
6	1, 5	sylbi 209	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
7		df-rab 3099	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
8	6, 7	eleq2s 2877	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 386   = wceq 1601  ∃wex 1823   ∈ wcel 2107  {cab 2763  {crab 3094

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-rab 3099

This theorem is referenced by:  elfvmptrab1  6567  elovmpt2rab  7157  elovmpt2rab1  7158  elovmpt3rab1  7170  mapfienlem1  8598  mapfienlem2  8599  mapfienlem3  8600  kmlem1  9307  fin1a2lem9  9565  nnind  11394  ublbneg  12080  supminf  12082  rlimrege0  14718  incexc2  14974  lcmgcdlem  15725  phisum  15899  prmgaplem5  16163  isinitoi  17038  istermoi  17039  odcl  18339  odlem2  18342  gexcl  18379  gexlem2  18381  gexdvds  18383  pgpssslw  18413  resspsrmul  19814  mplbas2  19867  mptcoe1fsupp  19981  psropprmul  20004  coe1mul2  20035  psgnfix2  20341  psgndiflemB  20342  psgndif  20344  copsgndif  20345  zrhcopsgndifOLD  20346  cpmatpmat  20922  mptcoe1matfsupp  21014  mp2pm2mplem4  21021  chpscmat  21054  chpscmatgsumbin  21056  chpscmatgsummon  21057  txdis1cn  21847  ptcmplem3  22266  rrxmvallem  23610  mdegmullem  24275  0sgm  25322  sgmf  25323  sgmnncl  25325  fsumdvdsdiaglem  25361  fsumdvdscom  25363  dvdsppwf1o  25364  dvdsflf1o  25365  musumsum  25370  muinv  25371  sgmppw  25374  rpvmasumlem  25628  dchrmusum2  25635  dchrvmasumlem1  25636  dchrvmasum2lem  25637  dchrisum0fmul  25647  dchrisum0ff  25648  dchrisum0flblem1  25649  dchrisum0  25661  logsqvma  25683  usgredg2v  26573  umgrres1lem  26657  upgrres1  26660  vtxdgoddnumeven  26901  rusgrnumwwlks  27354  rusgrnumwwlksOLD  27355  frgrwopreglem4  27723  frgrwopreg  27731  rabsnel  29903  nnindf  30129  ddemeas  30897  imambfm  30922  eulerpartlemgs2  31040  ballotlemfc0  31153  ballotlemfcc  31154  ballotlemirc  31192  reprf  31292  tgoldbachgnn  31339  tgoldbachgt  31343  bnj110  31527  poimirlem4  34039  poimirlem5  34040  poimirlem6  34041  poimirlem7  34042  poimirlem8  34043  poimirlem9  34044  poimirlem10  34045  poimirlem11  34046  poimirlem12  34047  poimirlem13  34048  poimirlem14  34049  poimirlem15  34050  poimirlem16  34051  poimirlem17  34052  poimirlem18  34053  poimirlem19  34054  poimirlem20  34055  poimirlem21  34056  poimirlem22  34057  poimirlem26  34061  mblfinlem2  34073  rencldnfilem  38344  irrapx1  38352  radcnvrat  39469  supminfxr  40599  fsumiunss  40715  dvnprodlem1  41089  stoweidlem15  41159  stoweidlem31  41175  fourierdlem25  41276  fourierdlem51  41301  fourierdlem79  41329  etransclem28  41406  issalgend  41480  sge0iunmptlemre  41556  hoidmvlelem2  41737  issmflem  41863  smfresal  41922  2zrngasgrp  42955  2zrngamnd  42956  2zrngacmnd  42957  2zrngagrp  42958  2zrngmsgrp  42962  2zrngALT  42963  2zrngnmlid  42964  2zrngnmlid2  42966