Theorem elrabi 3643

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 3395	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2846	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

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

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 3395

This theorem is referenced by:  ssrab2  4031  elfvmptrab1w  6957  elfvmptrab1  6958  elovmporab  7595  elovmporab1w  7596  elovmporab1  7597  elovmpt3rab1  7609  mapfienlem1  9295  mapfienlem2  9296  mapfienlem3  9297  kmlem1  10045  fin1a2lem9  10302  ac6num  10373  nnind  12146  ublbneg  12834  supminf  12836  rlimrege0  15486  incexc2  15745  lcmgcdlem  16517  phisum  16702  prmgaplem5  16967  isinitoi  17906  istermoi  17907  odcl  19415  odlem2  19418  gexcl  19459  gexlem2  19461  gexdvds  19463  pgpssslw  19493  psgnfix2  21506  psgndiflemB  21507  psgndif  21509  copsgndif  21510  psrbagf  21825  psrbagleadd1  21835  resspsrmul  21883  mplbas2  21947  mhpmulcl  22034  psdmul  22051  mptcoe1fsupp  22098  psropprmul  22120  coe1mul2  22153  rhmcomulmpl  22267  cpmatpmat  22595  mptcoe1matfsupp  22687  mp2pm2mplem4  22694  chpscmat  22727  chpscmatgsumbin  22729  chpscmatgsummon  22730  txdis1cn  23520  ptcmplem3  23939  rrxmvallem  25302  mdegmullem  25981  0sgm  27052  sgmf  27053  sgmnncl  27055  fsumdvdsdiaglem  27091  fsumdvdscom  27093  dvdsppwf1o  27094  dvdsflf1o  27095  musumsum  27100  muinv  27101  sgmppw  27106  rpvmasumlem  27396  dchrmusum2  27403  dchrvmasumlem1  27404  dchrvmasum2lem  27405  dchrisum0fmul  27415  dchrisum0ff  27416  dchrisum0flblem1  27417  dchrisum0  27429  logsqvma  27451  precsexlem9  28122  usgredg2v  29172  umgrres1lem  29255  upgrres1  29258  vtxdgoddnumeven  29499  rusgrnumwwlks  29919  frgrwopreglem4  30259  frgrwopreg  30267  rabsnel  32444  nnindf  32765  cyc3evpm  33093  cycpmgcl  33096  cycpmconjslem2  33098  elrgspnsubrun  33190  nsgmgclem  33349  ddemeas  34209  imambfm  34236  eulerpartlemgs2  34354  ballotlemfc0  34467  ballotlemfcc  34468  ballotlemirc  34506  reprf  34586  tgoldbachgnn  34633  tgoldbachgt  34637  bnj110  34831  fnrelpredd  35062  wevgblacfn  35092  weiunlem2  36447  poimirlem4  37614  poimirlem5  37615  poimirlem6  37616  poimirlem7  37617  poimirlem8  37618  poimirlem9  37619  poimirlem10  37620  poimirlem11  37621  poimirlem12  37622  poimirlem13  37623  poimirlem14  37624  poimirlem15  37625  poimirlem16  37626  poimirlem17  37627  poimirlem18  37628  poimirlem19  37629  poimirlem20  37630  poimirlem21  37631  poimirlem22  37632  poimirlem26  37636  mblfinlem2  37648  primrootsunit1  42080  hashscontpow1  42104  aks6d1c6lem2  42154  aks6d1c6lem3  42155  grpods  42177  rhmcomulpsr  42534  mhphflem  42579  mhphf  42580  rencldnfilem  42803  irrapx1  42811  scottelrankd  44230  radcnvrat  44297  supminfxr  45453  fsumiunss  45566  dvnprodlem1  45937  stoweidlem15  46006  stoweidlem31  46022  fourierdlem25  46123  fourierdlem51  46148  fourierdlem79  46176  etransclem28  46253  issalgend  46329  sge0iunmptlemre  46406  hoidmvlelem2  46587  issmflem  46718  smfresal  46779  2zrngasgrp  48240  2zrngamnd  48241  2zrngacmnd  48242  2zrngagrp  48243  2zrngmsgrp  48247  2zrngALT  48248  2zrngnmlid  48249  2zrngnmlid2  48251