Theorem elrabi 3640

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 2146, ax-11 2162, ax-12 2182. (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 2713	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 482	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2079	. . . . . . 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 1931	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
12	1, 11	sylbi 217	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
13		df-rab 3398	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2852	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  ∃wex 1780  [wsb 2067   ∈ wcel 2113  {cab 2712  {crab 3397

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 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398

This theorem is referenced by:  ssrab2  4030  elfvmptrab1w  6966  elfvmptrab1  6967  elovmporab  7602  elovmporab1w  7603  elovmporab1  7604  elovmpt3rab1  7616  mapfienlem1  9306  mapfienlem2  9307  mapfienlem3  9308  kmlem1  10059  fin1a2lem9  10316  ac6num  10387  nnind  12161  ublbneg  12844  supminf  12846  rlimrege0  15500  incexc2  15759  lcmgcdlem  16531  phisum  16716  prmgaplem5  16981  isinitoi  17921  istermoi  17922  odcl  19463  odlem2  19466  gexcl  19507  gexlem2  19509  gexdvds  19511  pgpssslw  19541  psgnfix2  21552  psgndiflemB  21553  psgndif  21555  copsgndif  21556  psrbagf  21872  psrbagleadd1  21882  resspsrmul  21929  mplbas2  21995  mhpmulcl  22090  psdmul  22107  mptcoe1fsupp  22154  psropprmul  22176  coe1mul2  22209  rhmcomulmpl  22324  cpmatpmat  22652  mptcoe1matfsupp  22744  mp2pm2mplem4  22751  chpscmat  22784  chpscmatgsumbin  22786  chpscmatgsummon  22787  txdis1cn  23577  ptcmplem3  23996  rrxmvallem  25358  mdegmullem  26037  0sgm  27108  sgmf  27109  sgmnncl  27111  fsumdvdsdiaglem  27147  fsumdvdscom  27149  dvdsppwf1o  27150  dvdsflf1o  27151  musumsum  27156  muinv  27157  sgmppw  27162  rpvmasumlem  27452  dchrmusum2  27459  dchrvmasumlem1  27460  dchrvmasum2lem  27461  dchrisum0fmul  27471  dchrisum0ff  27472  dchrisum0flblem1  27473  dchrisum0  27485  logsqvma  27507  precsexlem9  28183  usgredg2v  29249  umgrres1lem  29332  upgrres1  29335  vtxdgoddnumeven  29576  rusgrnumwwlks  29999  frgrwopreglem4  30339  frgrwopreg  30347  rabsnel  32524  nnindf  32849  cyc3evpm  33181  cycpmgcl  33184  cycpmconjslem2  33186  elrgspnsubrun  33280  nsgmgclem  33441  mplvrpmrhm  33661  ddemeas  34342  imambfm  34368  eulerpartlemgs2  34486  ballotlemfc0  34599  ballotlemfcc  34600  ballotlemirc  34638  reprf  34718  tgoldbachgnn  34765  tgoldbachgt  34769  bnj110  34963  fnrelpredd  35196  wevgblacfn  35252  weiunlem2  36606  poimirlem4  37764  poimirlem5  37765  poimirlem6  37766  poimirlem7  37767  poimirlem8  37768  poimirlem9  37769  poimirlem10  37770  poimirlem11  37771  poimirlem12  37772  poimirlem13  37773  poimirlem14  37774  poimirlem15  37775  poimirlem16  37776  poimirlem17  37777  poimirlem18  37778  poimirlem19  37779  poimirlem20  37780  poimirlem21  37781  poimirlem22  37782  poimirlem26  37786  mblfinlem2  37798  primrootsunit1  42290  hashscontpow1  42314  aks6d1c6lem2  42364  aks6d1c6lem3  42365  grpods  42387  rhmcomulpsr  42746  mhphflem  42781  mhphf  42782  rencldnfilem  43004  irrapx1  43012  scottelrankd  44430  radcnvrat  44497  supminfxr  45650  fsumiunss  45763  dvnprodlem1  46132  stoweidlem15  46201  stoweidlem31  46217  fourierdlem25  46318  fourierdlem51  46343  fourierdlem79  46371  etransclem28  46448  issalgend  46524  sge0iunmptlemre  46601  hoidmvlelem2  46782  issmflem  46913  smfresal  46974  2zrngasgrp  48434  2zrngamnd  48435  2zrngacmnd  48436  2zrngagrp  48437  2zrngmsgrp  48441  2zrngALT  48442  2zrngnmlid  48443  2zrngnmlid2  48445