Theorem elrabi 3674

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 2130, ax-11 2147, ax-12 2164. (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 2806	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}))
2		df-clab 2705	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 482	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2070	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → [𝑦 / 𝑥]𝑥 ∈ 𝑉)
5		clelsb1 2855	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉)
6	4, 5	sylib 217	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑦 ∈ 𝑉)
7	2, 6	sylbi 216	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝑦 ∈ 𝑉)
8		eleq1 2816	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
9	8	biimpa 476	. . . . 5 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → 𝐴 ∈ 𝑉)
10	7, 9	sylan2 592	. . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
11	10	exlimiv 1926	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
12	1, 11	sylbi 216	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
13		df-rab 3428	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2846	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1534  ∃wex 1774  [wsb 2060   ∈ wcel 2099  {cab 2704  {crab 3427

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3428

This theorem is referenced by:  ssrab2  4073  elfvmptrab1w  7026  elfvmptrab1  7027  elovmporab  7661  elovmporab1w  7662  elovmporab1  7663  elovmpt3rab1  7675  mapfienlem1  9420  mapfienlem2  9421  mapfienlem3  9422  kmlem1  10165  fin1a2lem9  10423  ac6num  10494  nnind  12252  ublbneg  12939  supminf  12941  rlimrege0  15547  incexc2  15808  lcmgcdlem  16568  phisum  16750  prmgaplem5  17015  isinitoi  17979  istermoi  17980  odcl  19482  odlem2  19485  gexcl  19526  gexlem2  19528  gexdvds  19530  pgpssslw  19560  psgnfix2  21518  psgndiflemB  21519  psgndif  21521  copsgndif  21522  psrbagf  21838  psrbagleadd1  21856  resspsrmul  21906  mplbas2  21967  mhpmulcl  22060  psdmul  22077  mptcoe1fsupp  22121  psropprmul  22143  coe1mul2  22175  cpmatpmat  22599  mptcoe1matfsupp  22691  mp2pm2mplem4  22698  chpscmat  22731  chpscmatgsumbin  22733  chpscmatgsummon  22734  txdis1cn  23526  ptcmplem3  23945  rrxmvallem  25319  mdegmullem  26001  0sgm  27063  sgmf  27064  sgmnncl  27066  fsumdvdsdiaglem  27102  fsumdvdscom  27104  dvdsppwf1o  27105  dvdsflf1o  27106  musumsum  27111  muinv  27112  sgmppw  27117  rpvmasumlem  27407  dchrmusum2  27414  dchrvmasumlem1  27415  dchrvmasum2lem  27416  dchrisum0fmul  27426  dchrisum0ff  27427  dchrisum0flblem1  27428  dchrisum0  27440  logsqvma  27462  precsexlem9  28100  usgredg2v  29027  umgrres1lem  29110  upgrres1  29113  vtxdgoddnumeven  29354  rusgrnumwwlks  29772  frgrwopreglem4  30112  frgrwopreg  30120  rabsnel  32284  nnindf  32564  cyc3evpm  32849  cycpmgcl  32852  cycpmconjslem2  32854  nsgmgclem  33061  ddemeas  33791  imambfm  33818  eulerpartlemgs2  33936  ballotlemfc0  34048  ballotlemfcc  34049  ballotlemirc  34087  reprf  34180  tgoldbachgnn  34227  tgoldbachgt  34231  bnj110  34425  fnrelpredd  34648  poimirlem4  37032  poimirlem5  37033  poimirlem6  37034  poimirlem7  37035  poimirlem8  37036  poimirlem9  37037  poimirlem10  37038  poimirlem11  37039  poimirlem12  37040  poimirlem13  37041  poimirlem14  37042  poimirlem15  37043  poimirlem16  37044  poimirlem17  37045  poimirlem18  37046  poimirlem19  37047  poimirlem20  37048  poimirlem21  37049  poimirlem22  37050  poimirlem26  37054  mblfinlem2  37066  primrootsunit1  41504  hashscontpow1  41525  aks6d1c6lem2  41575  aks6d1c6lem3  41576  mhphflem  41751  mhphf  41752  rencldnfilem  42162  irrapx1  42170  scottelrankd  43607  radcnvrat  43674  supminfxr  44769  fsumiunss  44886  dvnprodlem1  45257  stoweidlem15  45326  stoweidlem31  45342  fourierdlem25  45443  fourierdlem51  45468  fourierdlem79  45496  etransclem28  45573  issalgend  45649  sge0iunmptlemre  45726  hoidmvlelem2  45907  issmflem  46038  smfresal  46099  2zrngasgrp  47231  2zrngamnd  47232  2zrngacmnd  47233  2zrngagrp  47234  2zrngmsgrp  47238  2zrngALT  47239  2zrngnmlid  47240  2zrngnmlid2  47242