Theorem elab 3630

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 2144, ax-11 2160, ax-12 2180. (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 3627	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
4	1, 3	ax-mp 5	1 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2111  {cab 2709  Vcvv 3436

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-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806

This theorem is referenced by:  intab  4928  dfiun2g  4980  dfiin2g  4981  dfiunv2  4984  opeliunxp  5686  opeliun2xp  5687  dmopab2rex  5862  iotanul2  6460  elabrex  7182  abrexco  7184  uniuni  7701  finds  7832  finds2  7834  funcnvuni  7868  fiunlem  7880  fiun  7881  f1iun  7882  mapfset  8780  mapfoss  8782  fsetsspwxp  8783  mapval2  8802  sbthlem2  9007  ssenen  9070  dffi2  9313  dffi3  9321  tctr  9634  tcmin  9635  tc2  9636  tz9.13  9690  tcrank  9783  kardex  9793  karden  9794  cardf2  9842  cardiun  9881  alephval3  10007  dfac3  10018  dfac5lem3  10022  dfac5lem4  10023  dfac5lem4OLD  10025  dfac2b  10028  kmlem12  10059  cardcf  10149  cfeq0  10153  cfsuc  10154  cff1  10155  cflim2  10160  cfss  10162  axdc3lem2  10348  axdc3lem3  10349  axdclem  10416  brdom7disj  10428  brdom6disj  10429  tskuni  10680  gruina  10715  nqpr  10911  supadd  12096  supmul  12100  dfnn2  12144  dfuzi  12570  seqof  13972  hashfacen  14367  hashf1lem1  14368  hashf1lem2  14369  0csh0  14706  trclun  14927  dfrtrcl2  14975  shftfval  14983  infcvgaux1i  15770  sursubmefmnd  18810  injsubmefmnd  18811  smndex2dnrinv  18829  symg1bas  19309  pmtrprfvalrn  19406  psgnvali  19426  efgrelexlemb  19668  lss1d  20902  lidldvgen  21277  zndvds  21492  mpfind  22048  pf1ind  22276  cmpsublem  23320  cmpsub  23321  ptpjopn  23533  ptclsg  23536  txdis1cn  23556  tx1stc  23571  hauspwpwf1  23908  qustgplem  24042  ustn0  24142  i1fadd  25629  i1fmul  25630  i1fmulc  25637  nosupno  27648  nosupbnd1lem1  27653  noinfno  27663  addsproplem2  27919  addsproplem4  27921  addsproplem5  27922  addsproplem6  27923  addsuniflem  27950  negsid  27989  mulsproplem9  28069  mulsproplem12  28072  ssltmul1  28092  ssltmul2  28093  precsexlem9  28159  precsexlem11  28161  dfn0s2  28266  recut  28404  0reno  28405  ausgrusgri  29153  ushgredgedg  29214  ushgredgedgloop  29216  wspniunwspnon  29908  rusgrnumwwlkb0  29959  fusgr2wsp2nb  30321  nmosetn0  30752  nmoolb  30758  nmlno0lem  30780  nmopsetn0  31852  nmfnsetn0  31865  nmoplb  31894  nmfnlb  31911  nmlnop0iALT  31982  nmopun  32001  nmcexi  32013  branmfn  32092  pjnmopi  32135  fpwrelmapffslem  32722  ldlfcntref  33874  esumc  34071  orvcval2  34479  derangenlem  35222  satfrnmapom  35421  fmlaomn0  35441  fmlasucdisj  35450  dmopab3rexdif  35456  2goelgoanfmla1  35475  mclsssvlem  35613  mclsind  35621  dfon2lem3  35834  dfon2lem7  35838  fnimage  35978  imageval  35979  poimirlem4  37670  poimirlem5  37671  poimirlem6  37672  poimirlem7  37673  poimirlem8  37674  poimirlem9  37675  poimirlem10  37676  poimirlem11  37677  poimirlem12  37678  poimirlem13  37679  poimirlem14  37680  poimirlem15  37681  poimirlem16  37682  poimirlem17  37683  poimirlem18  37684  poimirlem19  37685  poimirlem20  37686  poimirlem21  37687  poimirlem22  37688  poimirlem25  37691  poimirlem26  37692  poimirlem27  37693  poimirlem29  37695  poimirlem31  37697  mblfinlem3  37705  mblfinlem4  37706  ismblfin  37707  itg2addnc  37720  sdclem2  37788  sdclem1  37789  heibor1lem  37855  glbconxN  39483  pmapglbx  39874  dvhb1dimN  41091  sticksstones10  42254  sticksstones11  42255  sticksstones12a  42256  sticksstones12  42257  sticksstones17  42262  sticksstones18  42263  sticksstones19  42264  redvmptabs  42459  abbibw  42776  eldiophss  42872  setindtrs  43123  hbtlem2  43222  hbtlem5  43226  rngunsnply  43267  oaun3lem1  43472  oadif1lem  43477  oadif1  43478  dftrcl3  43818  brtrclfv2  43825  dfrtrcl3  43831  dfhe3  43873  elscottab  44342  cpcolld  44356  nzss  44415  upbdrech  45411  fourierdlem36  46246  sge0resplit  46509  hoidmvlelem1  46698  fsetsniunop  47154  elsprel  47580  ixpv  48995  iinfconstbas  49172  setrec2lem1  49799