Theorem elab 3632

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  {cab 2738  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835

This theorem is used by:  intab  4937  dfiun2g  4987  dfiin2g  4988  dfiunv2  4991  opeliunxp  5714  opeliun2xp  5715  dmopab2rex  5895  iotanul2  6500  elabrex  7234  abrexco  7236  uniuni  7759  finds  7891  finds2  7893  funcnvuni  7927  fiunlem  7937  fiun  7938  f1iun  7939  mapfset  8850  mapfoss  8852  fsetsspwxp  8853  mapval2  8878  sbthlem2  9085  ssenen  9148  dffi2  9393  dffi3  9401  tctr  9717  tcmin  9718  tc2  9719  tz9.13  9773  tcrank  9874  elscottab  9913  kardexOLD  9929  kardenOLD  9931  setrec2lem1  9945  cardf2  9995  cardiun  10034  alephval3  10160  dfac3  10171  dfac5lem3  10175  dfac5lem4  10176  dfac2b  10180  kmlem12  10211  cardcf  10300  cfeq0  10305  cfsuc  10306  cff1  10307  cflim2  10312  cfss  10314  axdc3lem2  10500  axdc3lem3  10501  axdclem  10568  brdom7disj  10581  brdom6disj  10582  tskuni  10839  gruina  10874  nqpr  11070  supadd  12254  supmul  12258  dfnn2  12317  dfuzi  12759  seqof  14170  hashfacen  14566  hashf1lem1  14567  hashf1lem2  14568  0csh0  14911  trclun  15134  dfrtrcl2  15182  shftfval  15190  infcvgaux1i  15993  sursubmefmnd  19053  injsubmefmnd  19054  smndex2dnrinv  19075  symg1bas  19566  pmtrprfvalrn  19663  psgnvali  19683  efgrelexlemb  19925  lss1d  21199  lidldvgen  21619  zndvds  21816  mpfind  22385  pf1ind  22634  cmpsublem  23678  cmpsub  23679  ptpjopn  23892  ptclsg  23895  txdis1cn  23915  tx1stc  23930  hauspwpwf1  24267  qustgplem  24401  ustn0  24501  i1fadd  25977  i1fmul  25978  i1fmulc  25985  nosupno  27993  nosupbnd1lem1  27998  noinfno  28008  addsproplem2  28289  addsproplem4  28291  addsproplem5  28292  addsproplem6  28293  addsuniflem  28320  negsid  28360  mulsproplem9  28443  mulsproplem12  28446  sltmuls1  28466  sltmuls2  28467  precsexlem9  28534  precsexlem11  28536  dfn0s2  28651  recut  28813  elreno2  28814  ausgrusgri  29682  ushgredgedg  29743  ushgredgedgloop  29745  wspniunwspnon  30445  rusgrnumwwlkb0  30496  fusgr2wsp2nb  30868  nmosetn0  31300  nmoolb  31306  nmlno0lem  31328  nmopsetn0  32400  nmfnsetn0  32413  nmoplb  32442  nmfnlb  32459  nmlnop0iALT  32530  nmopun  32549  nmcexi  32561  branmfn  32640  pjnmopi  32683  fpwrelmapffslem  33257  ldlfcntref  34419  esumc  34616  orvcval2  35025  derangenlem  35857  satfrnmapom  36056  fmlaomn0  36076  fmlasucdisj  36085  dmopab3rexdif  36091  2goelgoanfmla1  36110  mclsssvlem  36248  mclsind  36256  dfon2lem3  36469  dfon2lem7  36473  fnimage  36613  imageval  36614  dfttc4  37240  poimirlem4  38462  poimirlem5  38463  poimirlem6  38464  poimirlem7  38465  poimirlem8  38466  poimirlem9  38467  poimirlem10  38468  poimirlem11  38469  poimirlem12  38470  poimirlem13  38471  poimirlem14  38472  poimirlem15  38473  poimirlem16  38474  poimirlem17  38475  poimirlem18  38476  poimirlem19  38477  poimirlem20  38478  poimirlem21  38479  poimirlem22  38480  poimirlem25  38483  poimirlem26  38484  poimirlem27  38485  poimirlem29  38487  poimirlem31  38489  mblfinlem3  38497  mblfinlem4  38498  ismblfin  38499  itg2addnc  38512  sdclem2  38596  sdclem1  38597  heibor1lem  38663  glbconxN  40355  pmapglbx  40746  dvhb1dimN  41963  sticksstones10  43125  sticksstones11  43126  sticksstones12a  43127  sticksstones12  43128  sticksstones17  43133  sticksstones18  43134  sticksstones19  43135  redvmptabs  43339  abbibw  43627  eldiophss  43723  setindtrs  43970  hbtlem2  44069  hbtlem5  44073  rngunsnply  44114  oaun3lem1  44319  oadif1lem  44324  oadif1  44325  dftrcl3  44664  brtrclfv2  44671  dfrtrcl3  44677  dfhe3  44719  cpcolld  45186  nzss  45245  upbdrech  46242  fourierdlem36  47075  sge0resplit  47338  hoidmvlelem1  47527  fsetsniunop  48041  elsprel  48479  ixpv  49920  iinfconstbas  50096