Theorem elrabi 3649

Description: Implication for the membership in a restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017.) Remove disjoint variable condition on 𝐴, 𝑥 and avoid ax-10 2178, ax-11 2194, ax-12 2215. (Revised by SN, 5-Aug-2024.)

Assertion

Ref	Expression
elrabi	⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Distinct variable group:   𝑥,𝑉

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem elrabi

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfclel 2841	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}))
2		df-clab 2744	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 487	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2110	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → [𝑦 / 𝑥]𝑥 ∈ 𝑉)
5		clelsb1 2892	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉)
6	4, 5	sylib 221	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑦 ∈ 𝑉)
7	2, 6	sylbi 220	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝑦 ∈ 𝑉)
8		eleq1 2853	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
9	8	biimpa 481	. . . . 5 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → 𝐴 ∈ 𝑉)
10	7, 9	sylan2 604	. . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
11	10	exlimiv 1953	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
12	1, 11	sylbi 220	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
13		df-rab 3418	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2883	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563  ∃wex 1802  [wsb 2093   ∈ wcel 2145  {cab 2743  {crab 3417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418

This theorem is referenced by:  ssrab2  4036  elfvmptrab1w  7007  elfvmptrab1  7008  elovmporab  7646  elovmporab1w  7647  elovmporab1  7648  elovmpt3rab1  7660  mapfienlem1  9353  mapfienlem2  9354  mapfienlem3  9355  scottelrankd  9861  kmlem1  10122  fin1a2lem9  10380  ac6num  10451  nnind  12242  ublbneg  12948  supminf  12950  rlimrege0  15620  incexc2  15882  lcmgcdlem  16654  phisum  16840  prmgaplem5  17105  isinitoi  18046  istermoi  18047  odcl  19597  odlem2  19600  gexcl  19641  gexlem2  19643  gexdvds  19645  pgpssslw  19675  psgnfix2  21709  psgndiflemB  21710  psgndif  21712  copsgndif  21713  psrbagf  22028  psrbagleadd1  22038  resspsrmul  22085  mplbas2  22153  rhmcomulmpl  22235  mhpmulcl  22272  psdmul  22289  mptcoe1fsupp  22335  psropprmul  22357  coe1mul2  22390  cpmatpmat  22828  mptcoe1matfsupp  22920  mp2pm2mplem4  22927  chpscmat  22960  chpscmatgsumbin  22962  chpscmatgsummon  22963  txdis1cn  23753  ptcmplem3  24172  rrxmvallem  25524  mdegmullem  26196  0sgm  27266  sgmf  27267  sgmnncl  27269  fsumdvdsdiaglem  27305  fsumdvdscom  27307  dvdsppwf1o  27308  dvdsflf1o  27309  musumsum  27314  muinv  27315  sgmppw  27319  rpvmasumlem  27609  dchrmusum2  27616  dchrvmasumlem1  27617  dchrvmasum2lem  27618  dchrisum0fmul  27628  dchrisum0ff  27629  dchrisum0flblem1  27630  dchrisum0  27642  logsqvma  27664  precsexlem9  28366  usgredg2v  29486  umgrres1lem  29569  upgrres1  29572  vtxdgoddnumeven  29812  rusgrnumwwlks  30235  frgrwopreglem4  30575  frgrwopreg  30583  rabsnel  32756  nnindf  33077  cyc3evpm  33383  cycpmgcl  33386  cycpmconjslem2  33388  elrgspnsubrun  33482  nsgmgclem  33636  mplvrpmrhm  33854  ddemeas  34543  imambfm  34569  eulerpartlemgs2  34687  ballotlemfc0  34800  ballotlemfcc  34801  ballotlemirc  34839  reprf  34916  tgoldbachgnn  34963  tgoldbachgt  34967  bnj110  35163  fnrelpredd  35397  wevgblacfn  35466  weiunlem  36836  poimirlem4  38135  poimirlem5  38136  poimirlem6  38137  poimirlem7  38138  poimirlem8  38139  poimirlem9  38140  poimirlem10  38141  poimirlem11  38142  poimirlem12  38143  poimirlem13  38144  poimirlem14  38145  poimirlem15  38146  poimirlem16  38147  poimirlem17  38148  poimirlem18  38149  poimirlem19  38150  poimirlem20  38151  poimirlem21  38152  poimirlem22  38153  poimirlem26  38157  mblfinlem2  38169  primrootsunit1  42726  hashscontpow1  42750  aks6d1c6lem2  42800  aks6d1c6lem3  42801  grpods  42823  rhmcomulpsr  43176  mhphflem  43190  mhphf  43191  rencldnfilem  43409  irrapx1  43417  radcnvrat  44888  supminfxr  46036  fsumiunss  46149  dvnprodlem1  46518  stoweidlem15  46587  stoweidlem31  46603  fourierdlem25  46704  fourierdlem51  46729  fourierdlem79  46757  etransclem28  46834  issalgend  46910  sge0iunmptlemre  46987  hoidmvlelem2  47168  issmflem  47299  smfresal  47360  2zrngasgrp  48866  2zrngamnd  48867  2zrngacmnd  48868  2zrngagrp  48869  2zrngmsgrp  48873  2zrngALT  48874  2zrngnmlid  48875  2zrngnmlid2  48877