Theorem elrabi 3638

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 2144, ax-11 2160, ax-12 2180. (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 2807	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}))
2		df-clab 2710	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 482	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2077	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → [𝑦 / 𝑥]𝑥 ∈ 𝑉)
5		clelsb1 2858	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉)
6	4, 5	sylib 218	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑦 ∈ 𝑉)
7	2, 6	sylbi 217	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝑦 ∈ 𝑉)
8		eleq1 2819	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
9	8	biimpa 476	. . . . 5 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → 𝐴 ∈ 𝑉)
10	7, 9	sylan2 593	. . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
11	10	exlimiv 1931	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
12	1, 11	sylbi 217	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
13		df-rab 3396	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2849	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  ∃wex 1780  [wsb 2067   ∈ wcel 2111  {cab 2709  {crab 3395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396

This theorem is referenced by:  ssrab2  4027  elfvmptrab1w  6956  elfvmptrab1  6957  elovmporab  7592  elovmporab1w  7593  elovmporab1  7594  elovmpt3rab1  7606  mapfienlem1  9289  mapfienlem2  9290  mapfienlem3  9291  kmlem1  10042  fin1a2lem9  10299  ac6num  10370  nnind  12143  ublbneg  12831  supminf  12833  rlimrege0  15486  incexc2  15745  lcmgcdlem  16517  phisum  16702  prmgaplem5  16967  isinitoi  17906  istermoi  17907  odcl  19448  odlem2  19451  gexcl  19492  gexlem2  19494  gexdvds  19496  pgpssslw  19526  psgnfix2  21536  psgndiflemB  21537  psgndif  21539  copsgndif  21540  psrbagf  21855  psrbagleadd1  21865  resspsrmul  21913  mplbas2  21977  mhpmulcl  22064  psdmul  22081  mptcoe1fsupp  22128  psropprmul  22150  coe1mul2  22183  rhmcomulmpl  22297  cpmatpmat  22625  mptcoe1matfsupp  22717  mp2pm2mplem4  22724  chpscmat  22757  chpscmatgsumbin  22759  chpscmatgsummon  22760  txdis1cn  23550  ptcmplem3  23969  rrxmvallem  25331  mdegmullem  26010  0sgm  27081  sgmf  27082  sgmnncl  27084  fsumdvdsdiaglem  27120  fsumdvdscom  27122  dvdsppwf1o  27123  dvdsflf1o  27124  musumsum  27129  muinv  27130  sgmppw  27135  rpvmasumlem  27425  dchrmusum2  27432  dchrvmasumlem1  27433  dchrvmasum2lem  27434  dchrisum0fmul  27444  dchrisum0ff  27445  dchrisum0flblem1  27446  dchrisum0  27458  logsqvma  27480  precsexlem9  28153  usgredg2v  29205  umgrres1lem  29288  upgrres1  29291  vtxdgoddnumeven  29532  rusgrnumwwlks  29955  frgrwopreglem4  30295  frgrwopreg  30303  rabsnel  32480  nnindf  32802  cyc3evpm  33119  cycpmgcl  33122  cycpmconjslem2  33124  elrgspnsubrun  33216  nsgmgclem  33376  mplvrpmrhm  33577  ddemeas  34249  imambfm  34275  eulerpartlemgs2  34393  ballotlemfc0  34506  ballotlemfcc  34507  ballotlemirc  34545  reprf  34625  tgoldbachgnn  34672  tgoldbachgt  34676  bnj110  34870  fnrelpredd  35102  wevgblacfn  35153  weiunlem2  36507  poimirlem4  37674  poimirlem5  37675  poimirlem6  37676  poimirlem7  37677  poimirlem8  37678  poimirlem9  37679  poimirlem10  37680  poimirlem11  37681  poimirlem12  37682  poimirlem13  37683  poimirlem14  37684  poimirlem15  37685  poimirlem16  37686  poimirlem17  37687  poimirlem18  37688  poimirlem19  37689  poimirlem20  37690  poimirlem21  37691  poimirlem22  37692  poimirlem26  37696  mblfinlem2  37708  primrootsunit1  42200  hashscontpow1  42224  aks6d1c6lem2  42274  aks6d1c6lem3  42275  grpods  42297  rhmcomulpsr  42654  mhphflem  42699  mhphf  42700  rencldnfilem  42923  irrapx1  42931  scottelrankd  44350  radcnvrat  44417  supminfxr  45572  fsumiunss  45685  dvnprodlem1  46054  stoweidlem15  46123  stoweidlem31  46139  fourierdlem25  46240  fourierdlem51  46265  fourierdlem79  46293  etransclem28  46370  issalgend  46446  sge0iunmptlemre  46523  hoidmvlelem2  46704  issmflem  46835  smfresal  46896  2zrngasgrp  48356  2zrngamnd  48357  2zrngacmnd  48358  2zrngagrp  48359  2zrngmsgrp  48363  2zrngALT  48364  2zrngnmlid  48365  2zrngnmlid2  48367