Theorem elrabi 3646

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 2176, ax-11 2192, ax-12 2213. (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 2839	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}))
2		df-clab 2742	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 487	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2108	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → [𝑦 / 𝑥]𝑥 ∈ 𝑉)
5		clelsb1 2890	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉)
6	4, 5	sylib 221	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑦 ∈ 𝑉)
7	2, 6	sylbi 220	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝑦 ∈ 𝑉)
8		eleq1 2851	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
9	8	biimpa 481	. . . . 5 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → 𝐴 ∈ 𝑉)
10	7, 9	sylan2 604	. . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
11	10	exlimiv 1960	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
12	1, 11	sylbi 220	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
13		df-rab 3417	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2881	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   = wceq 1570  ∃wex 1809  [wsb 2096   ∈ wcel 2143  {cab 2741  {crab 3416

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417

This theorem is used by:  ssrab2  4034  elfvmptrab1w  7017  elfvmptrab1  7018  elovmporab  7656  elovmporab1w  7657  elovmporab1  7658  elovmpt3rab1  7670  mapfienlem1  9361  mapfienlem2  9362  mapfienlem3  9363  scottelrankd  9873  kmlem1  10139  fin1a2lem9  10396  ac6num  10467  nnind  12255  ublbneg  12961  supminf  12963  rlimrege0  15635  incexc2  15897  lcmgcdlem  16668  phisum  16854  prmgaplem5  17119  isinitoi  18060  istermoi  18061  odcl  19610  odlem2  19613  gexcl  19654  gexlem2  19656  gexdvds  19658  pgpssslw  19688  psgnfix2  21758  psgndiflemB  21759  psgndif  21761  copsgndif  21762  psrbagf  22077  psrbagleadd1  22087  resspsrmul  22134  mplbas2  22202  rhmcomulmpl  22284  mhpmulcl  22321  psdmul  22338  mptcoe1fsupp  22384  psropprmul  22406  coe1mul2  22439  cpmatpmat  22876  mptcoe1matfsupp  22968  mp2pm2mplem4  22975  chpscmat  23008  chpscmatgsumbin  23010  chpscmatgsummon  23011  txdis1cn  23801  ptcmplem3  24220  rrxmvallem  25572  mdegmullem  26244  0sgm  27317  sgmf  27318  sgmnncl  27320  fsumdvdsdiaglem  27356  fsumdvdscom  27358  dvdsppwf1o  27359  dvdsflf1o  27360  musumsum  27365  muinv  27366  sgmppw  27370  rpvmasumlem  27660  dchrmusum2  27667  dchrvmasumlem1  27668  dchrvmasum2lem  27669  dchrisum0fmul  27679  dchrisum0ff  27680  dchrisum0flblem1  27681  dchrisum0  27693  logsqvma  27715  precsexlem9  28417  usgredg2v  29586  umgrres1lem  29669  upgrres1  29672  vtxdgoddnumeven  29912  rusgrnumwwlks  30335  frgrwopreglem4  30675  frgrwopreg  30683  rabsnel  32855  nnindf  33173  cyc3evpm  33479  cycpmgcl  33482  cycpmconjslem2  33484  elrgspnsubrun  33578  nsgmgclem  33729  mplvrpmrhm  33946  ddemeas  34635  imambfm  34661  eulerpartlemgs2  34779  ballotlemfc0  34892  ballotlemfcc  34893  ballotlemirc  34931  reprf  35008  tgoldbachgnn  35055  tgoldbachgt  35059  bnj110  35255  fnrelpredd  35491  wevgblacfn  35603  weiunlem  37002  poimirlem4  38303  poimirlem5  38304  poimirlem6  38305  poimirlem7  38306  poimirlem8  38307  poimirlem9  38308  poimirlem10  38309  poimirlem11  38310  poimirlem12  38311  poimirlem13  38312  poimirlem14  38313  poimirlem15  38314  poimirlem16  38315  poimirlem17  38316  poimirlem18  38317  poimirlem19  38318  poimirlem20  38319  poimirlem21  38320  poimirlem22  38321  poimirlem26  38325  mblfinlem2  38337  primrootsunit1  42892  hashscontpow1  42916  aks6d1c6lem2  42966  aks6d1c6lem3  42967  grpods  42989  rhmcomulpsr  43342  mhphflem  43356  mhphf  43357  rencldnfilem  43575  irrapx1  43583  radcnvrat  45052  supminfxr  46206  fsumiunss  46319  dvnprodlem1  46688  stoweidlem15  46757  stoweidlem31  46773  fourierdlem25  46874  fourierdlem51  46899  fourierdlem79  46927  etransclem28  47004  issalgend  47080  sge0iunmptlemre  47157  hoidmvlelem2  47338  issmflem  47469  smfresal  47530  2zrngasgrp  49039  2zrngamnd  49040  2zrngacmnd  49041  2zrngagrp  49042  2zrngmsgrp  49046  2zrngALT  49047  2zrngnmlid  49048  2zrngnmlid2  49050