Theorem elrabi 3666

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 2810	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}))
2		df-clab 2714	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 482	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2074	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → [𝑦 / 𝑥]𝑥 ∈ 𝑉)
5		clelsb1 2861	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉)
6	4, 5	sylib 218	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑦 ∈ 𝑉)
7	2, 6	sylbi 217	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝑦 ∈ 𝑉)
8		eleq1 2822	. . . . . 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 3416	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2852	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416

This theorem is referenced by:  ssrab2  4055  elfvmptrab1w  7013  elfvmptrab1  7014  elovmporab  7653  elovmporab1w  7654  elovmporab1  7655  elovmpt3rab1  7667  mapfienlem1  9417  mapfienlem2  9418  mapfienlem3  9419  kmlem1  10165  fin1a2lem9  10422  ac6num  10493  nnind  12258  ublbneg  12949  supminf  12951  rlimrege0  15595  incexc2  15854  lcmgcdlem  16625  phisum  16810  prmgaplem5  17075  isinitoi  18012  istermoi  18013  odcl  19517  odlem2  19520  gexcl  19561  gexlem2  19563  gexdvds  19565  pgpssslw  19595  psgnfix2  21559  psgndiflemB  21560  psgndif  21562  copsgndif  21563  psrbagf  21878  psrbagleadd1  21888  resspsrmul  21936  mplbas2  22000  mhpmulcl  22087  psdmul  22104  mptcoe1fsupp  22151  psropprmul  22173  coe1mul2  22206  rhmcomulmpl  22320  cpmatpmat  22648  mptcoe1matfsupp  22740  mp2pm2mplem4  22747  chpscmat  22780  chpscmatgsumbin  22782  chpscmatgsummon  22783  txdis1cn  23573  ptcmplem3  23992  rrxmvallem  25356  mdegmullem  26035  0sgm  27106  sgmf  27107  sgmnncl  27109  fsumdvdsdiaglem  27145  fsumdvdscom  27147  dvdsppwf1o  27148  dvdsflf1o  27149  musumsum  27154  muinv  27155  sgmppw  27160  rpvmasumlem  27450  dchrmusum2  27457  dchrvmasumlem1  27458  dchrvmasum2lem  27459  dchrisum0fmul  27469  dchrisum0ff  27470  dchrisum0flblem1  27471  dchrisum0  27483  logsqvma  27505  precsexlem9  28169  usgredg2v  29206  umgrres1lem  29289  upgrres1  29292  vtxdgoddnumeven  29533  rusgrnumwwlks  29956  frgrwopreglem4  30296  frgrwopreg  30304  rabsnel  32481  nnindf  32798  cyc3evpm  33161  cycpmgcl  33164  cycpmconjslem2  33166  elrgspnsubrun  33244  nsgmgclem  33426  ddemeas  34267  imambfm  34294  eulerpartlemgs2  34412  ballotlemfc0  34525  ballotlemfcc  34526  ballotlemirc  34564  reprf  34644  tgoldbachgnn  34691  tgoldbachgt  34695  bnj110  34889  fnrelpredd  35120  wevgblacfn  35131  weiunlem2  36481  poimirlem4  37648  poimirlem5  37649  poimirlem6  37650  poimirlem7  37651  poimirlem8  37652  poimirlem9  37653  poimirlem10  37654  poimirlem11  37655  poimirlem12  37656  poimirlem13  37657  poimirlem14  37658  poimirlem15  37659  poimirlem16  37660  poimirlem17  37661  poimirlem18  37662  poimirlem19  37663  poimirlem20  37664  poimirlem21  37665  poimirlem22  37666  poimirlem26  37670  mblfinlem2  37682  primrootsunit1  42110  hashscontpow1  42134  aks6d1c6lem2  42184  aks6d1c6lem3  42185  grpods  42207  rhmcomulpsr  42574  mhphflem  42619  mhphf  42620  rencldnfilem  42843  irrapx1  42851  scottelrankd  44271  radcnvrat  44338  supminfxr  45491  fsumiunss  45604  dvnprodlem1  45975  stoweidlem15  46044  stoweidlem31  46060  fourierdlem25  46161  fourierdlem51  46186  fourierdlem79  46214  etransclem28  46291  issalgend  46367  sge0iunmptlemre  46444  hoidmvlelem2  46625  issmflem  46756  smfresal  46817  2zrngasgrp  48221  2zrngamnd  48222  2zrngacmnd  48223  2zrngagrp  48224  2zrngmsgrp  48228  2zrngALT  48229  2zrngnmlid  48230  2zrngnmlid2  48232