Theorem elab 3665

Description: Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. (Contributed by NM, 1-Aug-1994.) Avoid ax-10 2129, ax-11 2146, ax-12 2166. (Revised by SN, 5-Oct-2024.)

Hypotheses

Ref	Expression
elab.1	⊢ 𝐴 ∈ V
elab.2	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
elab	⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)

Distinct variable groups:   𝜓,𝑥   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem elab

Step	Hyp	Ref	Expression
1		elab.1	. 2 ⊢ 𝐴 ∈ V
2		elab.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	elabg 3663	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
4	1, 3	ax-mp 5	1 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533   ∈ wcel 2098  {cab 2702  Vcvv 3463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802

This theorem is referenced by:  ralabOLD  3685  rexabOLD  3688  intab  4981  dfiun2g  5033  dfiin2g  5035  dfiunv2  5038  opeliunxp  5744  dmopab2rex  5919  iotanul2  6517  elabrex  7250  abrexco  7252  uniuni  7763  finds  7902  finds2  7904  funcnvuni  7938  fiunlem  7944  fiun  7945  f1iun  7946  mapfset  8867  mapfoss  8869  fsetsspwxp  8870  mapval2  8889  sbthlem2  9107  ssenen  9174  dffi2  9446  dffi3  9454  tctr  9763  tcmin  9764  tc2  9765  tz9.13  9814  tcrank  9907  kardex  9917  karden  9918  cardf2  9966  cardiun  10005  alephval3  10133  dfac3  10144  dfac5lem3  10148  dfac5lem4  10149  dfac2b  10153  kmlem12  10184  cardcf  10275  cfeq0  10279  cfsuc  10280  cff1  10281  cflim2  10286  cfss  10288  axdc3lem2  10474  axdc3lem3  10475  axdclem  10542  brdom7disj  10554  brdom6disj  10555  tskuni  10806  gruina  10841  nqpr  11037  supadd  12212  supmul  12216  dfnn2  12255  dfuzi  12683  seqof  14056  hashfacen  14445  hashfacenOLD  14446  hashf1lem1  14447  hashf1lem1OLD  14448  hashf1lem2  14449  0csh0  14775  trclun  14993  dfrtrcl2  15041  shftfval  15049  infcvgaux1i  15835  sursubmefmnd  18852  injsubmefmnd  18853  smndex2dnrinv  18871  symg1bas  19349  pmtrprfvalrn  19447  psgnvali  19467  efgrelexlemb  19709  lss1d  20851  lidldvgen  21228  zndvds  21487  mpfind  22060  pf1ind  22283  cmpsublem  23333  cmpsub  23334  ptpjopn  23546  ptclsg  23549  txdis1cn  23569  tx1stc  23584  hauspwpwf1  23921  qustgplem  24055  ustn0  24155  i1fadd  25654  i1fmul  25655  i1fmulc  25663  nosupno  27666  nosupbnd1lem1  27671  noinfno  27681  addsproplem2  27917  addsproplem4  27919  addsproplem5  27920  addsproplem6  27921  addsuniflem  27948  negsid  27983  mulsproplem9  28058  mulsproplem12  28061  ssltmul1  28081  ssltmul2  28082  precsexlem9  28147  precsexlem11  28149  dfn0s2  28237  recut  28280  0reno  28281  ausgrusgri  29037  ushgredgedg  29098  ushgredgedgloop  29100  wspniunwspnon  29790  rusgrnumwwlkb0  29838  fusgr2wsp2nb  30200  nmosetn0  30631  nmoolb  30637  nmlno0lem  30659  nmopsetn0  31731  nmfnsetn0  31744  nmoplb  31773  nmfnlb  31790  nmlnop0iALT  31861  nmopun  31880  nmcexi  31892  branmfn  31971  pjnmopi  32014  fpwrelmapffslem  32571  ldlfcntref  33525  esumc  33740  orvcval2  34148  derangenlem  34851  satfrnmapom  35050  fmlaomn0  35070  fmlasucdisj  35079  dmopab3rexdif  35085  2goelgoanfmla1  35104  mclsssvlem  35242  mclsind  35250  dfon2lem3  35451  dfon2lem7  35455  fnimage  35595  imageval  35596  poimirlem4  37167  poimirlem5  37168  poimirlem6  37169  poimirlem7  37170  poimirlem8  37171  poimirlem9  37172  poimirlem10  37173  poimirlem11  37174  poimirlem12  37175  poimirlem13  37176  poimirlem14  37177  poimirlem15  37178  poimirlem16  37179  poimirlem17  37180  poimirlem18  37181  poimirlem19  37182  poimirlem20  37183  poimirlem21  37184  poimirlem22  37185  poimirlem25  37188  poimirlem26  37189  poimirlem27  37190  poimirlem29  37192  poimirlem31  37194  mblfinlem3  37202  mblfinlem4  37203  ismblfin  37204  itg2addnc  37217  sdclem2  37285  sdclem1  37286  heibor1lem  37352  glbconxN  38920  pmapglbx  39311  dvhb1dimN  40528  sticksstones10  41696  sticksstones11  41697  sticksstones12a  41698  sticksstones12  41699  sticksstones17  41704  sticksstones18  41705  sticksstones19  41706  eldiophss  42259  setindtrs  42511  hbtlem2  42613  hbtlem5  42617  rngunsnply  42662  oaun3lem1  42868  oadif1lem  42873  oadif1  42874  dftrcl3  43215  brtrclfv2  43222  dfrtrcl3  43228  dfhe3  43270  elscottab  43746  cpcolld  43760  nzss  43819  upbdrech  44750  fourierdlem36  45594  sge0resplit  45857  hoidmvlelem1  46046  fsetsniunop  46494  elsprel  46878  opeliun2xp  47508  setrec2lem1  48236