Theorem elrabi 3654

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 2142, ax-11 2158, ax-12 2178. (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 2804	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}))
2		df-clab 2708	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 482	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2075	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → [𝑦 / 𝑥]𝑥 ∈ 𝑉)
5		clelsb1 2855	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉)
6	4, 5	sylib 218	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑦 ∈ 𝑉)
7	2, 6	sylbi 217	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝑦 ∈ 𝑉)
8		eleq1 2816	. . . . . 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 3406	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2846	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ∃wex 1779  [wsb 2065   ∈ wcel 2109  {cab 2707  {crab 3405

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406

This theorem is referenced by:  ssrab2  4043  elfvmptrab1w  6995  elfvmptrab1  6996  elovmporab  7635  elovmporab1w  7636  elovmporab1  7637  elovmpt3rab1  7649  mapfienlem1  9356  mapfienlem2  9357  mapfienlem3  9358  kmlem1  10104  fin1a2lem9  10361  ac6num  10432  nnind  12204  ublbneg  12892  supminf  12894  rlimrege0  15545  incexc2  15804  lcmgcdlem  16576  phisum  16761  prmgaplem5  17026  isinitoi  17961  istermoi  17962  odcl  19466  odlem2  19469  gexcl  19510  gexlem2  19512  gexdvds  19514  pgpssslw  19544  psgnfix2  21508  psgndiflemB  21509  psgndif  21511  copsgndif  21512  psrbagf  21827  psrbagleadd1  21837  resspsrmul  21885  mplbas2  21949  mhpmulcl  22036  psdmul  22053  mptcoe1fsupp  22100  psropprmul  22122  coe1mul2  22155  rhmcomulmpl  22269  cpmatpmat  22597  mptcoe1matfsupp  22689  mp2pm2mplem4  22696  chpscmat  22729  chpscmatgsumbin  22731  chpscmatgsummon  22732  txdis1cn  23522  ptcmplem3  23941  rrxmvallem  25304  mdegmullem  25983  0sgm  27054  sgmf  27055  sgmnncl  27057  fsumdvdsdiaglem  27093  fsumdvdscom  27095  dvdsppwf1o  27096  dvdsflf1o  27097  musumsum  27102  muinv  27103  sgmppw  27108  rpvmasumlem  27398  dchrmusum2  27405  dchrvmasumlem1  27406  dchrvmasum2lem  27407  dchrisum0fmul  27417  dchrisum0ff  27418  dchrisum0flblem1  27419  dchrisum0  27431  logsqvma  27453  precsexlem9  28117  usgredg2v  29154  umgrres1lem  29237  upgrres1  29240  vtxdgoddnumeven  29481  rusgrnumwwlks  29904  frgrwopreglem4  30244  frgrwopreg  30252  rabsnel  32429  nnindf  32744  cyc3evpm  33107  cycpmgcl  33110  cycpmconjslem2  33112  elrgspnsubrun  33200  nsgmgclem  33382  ddemeas  34226  imambfm  34253  eulerpartlemgs2  34371  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemirc  34523  reprf  34603  tgoldbachgnn  34650  tgoldbachgt  34654  bnj110  34848  fnrelpredd  35079  wevgblacfn  35096  weiunlem2  36451  poimirlem4  37618  poimirlem5  37619  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem9  37623  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem13  37627  poimirlem14  37628  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem18  37632  poimirlem19  37633  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem26  37640  mblfinlem2  37652  primrootsunit1  42085  hashscontpow1  42109  aks6d1c6lem2  42159  aks6d1c6lem3  42160  grpods  42182  rhmcomulpsr  42539  mhphflem  42584  mhphf  42585  rencldnfilem  42808  irrapx1  42816  scottelrankd  44236  radcnvrat  44303  supminfxr  45460  fsumiunss  45573  dvnprodlem1  45944  stoweidlem15  46013  stoweidlem31  46029  fourierdlem25  46130  fourierdlem51  46155  fourierdlem79  46183  etransclem28  46260  issalgend  46336  sge0iunmptlemre  46413  hoidmvlelem2  46594  issmflem  46725  smfresal  46786  2zrngasgrp  48234  2zrngamnd  48235  2zrngacmnd  48236  2zrngagrp  48237  2zrngmsgrp  48241  2zrngALT  48242  2zrngnmlid  48243  2zrngnmlid2  48245