Theorem elrabi 3690

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 2139, ax-11 2155, ax-12 2175. (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 2815	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}))
2		df-clab 2713	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 482	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2072	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → [𝑦 / 𝑥]𝑥 ∈ 𝑉)
5		clelsb1 2866	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉)
6	4, 5	sylib 218	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑦 ∈ 𝑉)
7	2, 6	sylbi 217	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝑦 ∈ 𝑉)
8		eleq1 2827	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
9	8	biimpa 476	. . . . 5 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → 𝐴 ∈ 𝑉)
10	7, 9	sylan2 593	. . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
11	10	exlimiv 1928	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
12	1, 11	sylbi 217	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
13		df-rab 3434	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2857	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537  ∃wex 1776  [wsb 2062   ∈ wcel 2106  {cab 2712  {crab 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434

This theorem is referenced by:  ssrab2  4090  elfvmptrab1w  7043  elfvmptrab1  7044  elovmporab  7679  elovmporab1w  7680  elovmporab1  7681  elovmpt3rab1  7693  mapfienlem1  9443  mapfienlem2  9444  mapfienlem3  9445  kmlem1  10189  fin1a2lem9  10446  ac6num  10517  nnind  12282  ublbneg  12973  supminf  12975  rlimrege0  15612  incexc2  15871  lcmgcdlem  16640  phisum  16824  prmgaplem5  17089  isinitoi  18053  istermoi  18054  odcl  19569  odlem2  19572  gexcl  19613  gexlem2  19615  gexdvds  19617  pgpssslw  19647  psgnfix2  21635  psgndiflemB  21636  psgndif  21638  copsgndif  21639  psrbagf  21956  psrbagleadd1  21966  resspsrmul  22014  mplbas2  22078  mhpmulcl  22171  psdmul  22188  mptcoe1fsupp  22233  psropprmul  22255  coe1mul2  22288  rhmcomulmpl  22402  cpmatpmat  22732  mptcoe1matfsupp  22824  mp2pm2mplem4  22831  chpscmat  22864  chpscmatgsumbin  22866  chpscmatgsummon  22867  txdis1cn  23659  ptcmplem3  24078  rrxmvallem  25452  mdegmullem  26132  0sgm  27202  sgmf  27203  sgmnncl  27205  fsumdvdsdiaglem  27241  fsumdvdscom  27243  dvdsppwf1o  27244  dvdsflf1o  27245  musumsum  27250  muinv  27251  sgmppw  27256  rpvmasumlem  27546  dchrmusum2  27553  dchrvmasumlem1  27554  dchrvmasum2lem  27555  dchrisum0fmul  27565  dchrisum0ff  27566  dchrisum0flblem1  27567  dchrisum0  27579  logsqvma  27601  precsexlem9  28254  usgredg2v  29259  umgrres1lem  29342  upgrres1  29345  vtxdgoddnumeven  29586  rusgrnumwwlks  30004  frgrwopreglem4  30344  frgrwopreg  30352  rabsnel  32528  nnindf  32826  cyc3evpm  33153  cycpmgcl  33156  cycpmconjslem2  33158  nsgmgclem  33419  ddemeas  34217  imambfm  34244  eulerpartlemgs2  34362  ballotlemfc0  34474  ballotlemfcc  34475  ballotlemirc  34513  reprf  34606  tgoldbachgnn  34653  tgoldbachgt  34657  bnj110  34851  fnrelpredd  35082  wevgblacfn  35093  weiunlem2  36446  poimirlem4  37611  poimirlem5  37612  poimirlem6  37613  poimirlem7  37614  poimirlem8  37615  poimirlem9  37616  poimirlem10  37617  poimirlem11  37618  poimirlem12  37619  poimirlem13  37620  poimirlem14  37621  poimirlem15  37622  poimirlem16  37623  poimirlem17  37624  poimirlem18  37625  poimirlem19  37626  poimirlem20  37627  poimirlem21  37628  poimirlem22  37629  poimirlem26  37633  mblfinlem2  37645  primrootsunit1  42079  hashscontpow1  42103  aks6d1c6lem2  42153  aks6d1c6lem3  42154  grpods  42176  rhmcomulpsr  42538  mhphflem  42583  mhphf  42584  rencldnfilem  42808  irrapx1  42816  scottelrankd  44243  radcnvrat  44310  supminfxr  45414  fsumiunss  45531  dvnprodlem1  45902  stoweidlem15  45971  stoweidlem31  45987  fourierdlem25  46088  fourierdlem51  46113  fourierdlem79  46141  etransclem28  46218  issalgend  46294  sge0iunmptlemre  46371  hoidmvlelem2  46552  issmflem  46683  smfresal  46744  2zrngasgrp  48090  2zrngamnd  48091  2zrngacmnd  48092  2zrngagrp  48093  2zrngmsgrp  48097  2zrngALT  48098  2zrngnmlid  48099  2zrngnmlid2  48101