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 2130, ax-11 2147, ax-12 2164. (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 1534   ∈ wcel 2099  {cab 2704  Vcvv 3469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805

This theorem is referenced by:  ralabOLD  3685  rexabOLD  3688  intab  4976  dfiun2g  5027  dfiin2g  5029  dfiunv2  5032  opeliunxp  5739  dmopab2rex  5914  iotanul2  6512  elabrex  7246  abrexco  7248  uniuni  7758  finds  7898  finds2  7900  funcnvuni  7933  fiunlem  7939  fiun  7940  f1iun  7941  mapfset  8860  mapfoss  8862  fsetsspwxp  8863  mapval2  8882  sbthlem2  9100  ssenen  9167  dffi2  9438  dffi3  9446  tctr  9755  tcmin  9756  tc2  9757  tz9.13  9806  tcrank  9899  kardex  9909  karden  9910  cardf2  9958  cardiun  9997  alephval3  10125  dfac3  10136  dfac5lem3  10140  dfac5lem4  10141  dfac2b  10145  kmlem12  10176  cardcf  10267  cfeq0  10271  cfsuc  10272  cff1  10273  cflim2  10278  cfss  10280  axdc3lem2  10466  axdc3lem3  10467  axdclem  10534  brdom7disj  10546  brdom6disj  10547  tskuni  10798  gruina  10833  nqpr  11029  supadd  12204  supmul  12208  dfnn2  12247  dfuzi  12675  seqof  14048  hashfacen  14437  hashfacenOLD  14438  hashf1lem1  14439  hashf1lem1OLD  14440  hashf1lem2  14441  0csh0  14767  trclun  14985  dfrtrcl2  15033  shftfval  15041  infcvgaux1i  15827  sursubmefmnd  18839  injsubmefmnd  18840  smndex2dnrinv  18858  symg1bas  19336  pmtrprfvalrn  19434  psgnvali  19454  efgrelexlemb  19696  lss1d  20836  lidldvgen  21213  zndvds  21470  mpfind  22040  pf1ind  22261  cmpsublem  23290  cmpsub  23291  ptpjopn  23503  ptclsg  23506  txdis1cn  23526  tx1stc  23541  hauspwpwf1  23878  qustgplem  24012  ustn0  24112  i1fadd  25611  i1fmul  25612  i1fmulc  25620  nosupno  27623  nosupbnd1lem1  27628  noinfno  27638  addsproplem2  27874  addsproplem4  27876  addsproplem5  27877  addsproplem6  27878  addsuniflem  27905  negsid  27940  mulsproplem9  28011  mulsproplem12  28014  ssltmul1  28034  ssltmul2  28035  precsexlem9  28100  precsexlem11  28102  dfn0s2  28188  recut  28211  0reno  28212  ausgrusgri  28968  ushgredgedg  29029  ushgredgedgloop  29031  wspniunwspnon  29721  rusgrnumwwlkb0  29769  fusgr2wsp2nb  30131  nmosetn0  30562  nmoolb  30568  nmlno0lem  30590  nmopsetn0  31662  nmfnsetn0  31675  nmoplb  31704  nmfnlb  31721  nmlnop0iALT  31792  nmopun  31811  nmcexi  31823  branmfn  31902  pjnmopi  31945  fpwrelmapffslem  32498  ldlfcntref  33391  esumc  33606  orvcval2  34014  derangenlem  34717  satfrnmapom  34916  fmlaomn0  34936  fmlasucdisj  34945  dmopab3rexdif  34951  2goelgoanfmla1  34970  mclsssvlem  35108  mclsind  35116  dfon2lem3  35317  dfon2lem7  35321  fnimage  35461  imageval  35462  poimirlem4  37032  poimirlem5  37033  poimirlem6  37034  poimirlem7  37035  poimirlem8  37036  poimirlem9  37037  poimirlem10  37038  poimirlem11  37039  poimirlem12  37040  poimirlem13  37041  poimirlem14  37042  poimirlem15  37043  poimirlem16  37044  poimirlem17  37045  poimirlem18  37046  poimirlem19  37047  poimirlem20  37048  poimirlem21  37049  poimirlem22  37050  poimirlem25  37053  poimirlem26  37054  poimirlem27  37055  poimirlem29  37057  poimirlem31  37059  mblfinlem3  37067  mblfinlem4  37068  ismblfin  37069  itg2addnc  37082  sdclem2  37150  sdclem1  37151  heibor1lem  37217  glbconxN  38788  pmapglbx  39179  dvhb1dimN  40396  sticksstones10  41559  sticksstones11  41560  sticksstones12a  41561  sticksstones12  41562  sticksstones17  41567  sticksstones18  41568  sticksstones19  41569  eldiophss  42116  setindtrs  42368  hbtlem2  42470  hbtlem5  42474  rngunsnply  42519  oaun3lem1  42726  oadif1lem  42731  oadif1  42732  dftrcl3  43073  brtrclfv2  43080  dfrtrcl3  43086  dfhe3  43128  elscottab  43604  cpcolld  43618  nzss  43677  upbdrech  44610  fourierdlem36  45454  sge0resplit  45717  hoidmvlelem1  45906  fsetsniunop  46354  elsprel  46738  opeliun2xp  47319  setrec2lem1  48047