Theorem elrabi 3687

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 2141, ax-11 2157, ax-12 2177. (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 2817	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}))
2		df-clab 2715	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 482	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2074	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → [𝑦 / 𝑥]𝑥 ∈ 𝑉)
5		clelsb1 2868	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉)
6	4, 5	sylib 218	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑦 ∈ 𝑉)
7	2, 6	sylbi 217	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝑦 ∈ 𝑉)
8		eleq1 2829	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
9	8	biimpa 476	. . . . 5 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → 𝐴 ∈ 𝑉)
10	7, 9	sylan2 593	. . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
11	10	exlimiv 1930	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
12	1, 11	sylbi 217	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
13		df-rab 3437	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2859	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ∃wex 1779  [wsb 2064   ∈ wcel 2108  {cab 2714  {crab 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437

This theorem is referenced by:  ssrab2  4080  elfvmptrab1w  7043  elfvmptrab1  7044  elovmporab  7679  elovmporab1w  7680  elovmporab1  7681  elovmpt3rab1  7693  mapfienlem1  9445  mapfienlem2  9446  mapfienlem3  9447  kmlem1  10191  fin1a2lem9  10448  ac6num  10519  nnind  12284  ublbneg  12975  supminf  12977  rlimrege0  15615  incexc2  15874  lcmgcdlem  16643  phisum  16828  prmgaplem5  17093  isinitoi  18044  istermoi  18045  odcl  19554  odlem2  19557  gexcl  19598  gexlem2  19600  gexdvds  19602  pgpssslw  19632  psgnfix2  21617  psgndiflemB  21618  psgndif  21620  copsgndif  21621  psrbagf  21938  psrbagleadd1  21948  resspsrmul  21996  mplbas2  22060  mhpmulcl  22153  psdmul  22170  mptcoe1fsupp  22217  psropprmul  22239  coe1mul2  22272  rhmcomulmpl  22386  cpmatpmat  22716  mptcoe1matfsupp  22808  mp2pm2mplem4  22815  chpscmat  22848  chpscmatgsumbin  22850  chpscmatgsummon  22851  txdis1cn  23643  ptcmplem3  24062  rrxmvallem  25438  mdegmullem  26117  0sgm  27187  sgmf  27188  sgmnncl  27190  fsumdvdsdiaglem  27226  fsumdvdscom  27228  dvdsppwf1o  27229  dvdsflf1o  27230  musumsum  27235  muinv  27236  sgmppw  27241  rpvmasumlem  27531  dchrmusum2  27538  dchrvmasumlem1  27539  dchrvmasum2lem  27540  dchrisum0fmul  27550  dchrisum0ff  27551  dchrisum0flblem1  27552  dchrisum0  27564  logsqvma  27586  precsexlem9  28239  usgredg2v  29244  umgrres1lem  29327  upgrres1  29330  vtxdgoddnumeven  29571  rusgrnumwwlks  29994  frgrwopreglem4  30334  frgrwopreg  30342  rabsnel  32519  nnindf  32821  cyc3evpm  33170  cycpmgcl  33173  cycpmconjslem2  33175  elrgspnsubrun  33253  nsgmgclem  33439  ddemeas  34237  imambfm  34264  eulerpartlemgs2  34382  ballotlemfc0  34495  ballotlemfcc  34496  ballotlemirc  34534  reprf  34627  tgoldbachgnn  34674  tgoldbachgt  34678  bnj110  34872  fnrelpredd  35103  wevgblacfn  35114  weiunlem2  36464  poimirlem4  37631  poimirlem5  37632  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem9  37636  poimirlem10  37637  poimirlem11  37638  poimirlem12  37639  poimirlem13  37640  poimirlem14  37641  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem18  37645  poimirlem19  37646  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem26  37653  mblfinlem2  37665  primrootsunit1  42098  hashscontpow1  42122  aks6d1c6lem2  42172  aks6d1c6lem3  42173  grpods  42195  rhmcomulpsr  42561  mhphflem  42606  mhphf  42607  rencldnfilem  42831  irrapx1  42839  scottelrankd  44266  radcnvrat  44333  supminfxr  45475  fsumiunss  45590  dvnprodlem1  45961  stoweidlem15  46030  stoweidlem31  46046  fourierdlem25  46147  fourierdlem51  46172  fourierdlem79  46200  etransclem28  46277  issalgend  46353  sge0iunmptlemre  46430  hoidmvlelem2  46611  issmflem  46742  smfresal  46803  2zrngasgrp  48162  2zrngamnd  48163  2zrngacmnd  48164  2zrngagrp  48165  2zrngmsgrp  48169  2zrngALT  48170  2zrngnmlid  48171  2zrngnmlid2  48173