Theorem elab 3636

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 2215. (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 3633	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
4	1, 3	ax-mp 5	1 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)

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

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837

This theorem is used by:  intab  4941  dfiun2g  4992  dfiin2g  4993  dfiunv2  4996  opeliunxp  5726  opeliun2xp  5727  dmopab2rex  5905  iotanul2  6510  elabrex  7242  abrexco  7244  uniuni  7764  finds  7896  finds2  7898  funcnvuni  7932  fiunlem  7942  fiun  7943  f1iun  7944  mapfset  8854  mapfoss  8856  fsetsspwxp  8857  mapval2  8882  sbthlem2  9089  ssenen  9152  dffi2  9396  dffi3  9404  tctr  9720  tcmin  9721  tc2  9722  tz9.13  9776  tcrank  9869  elscottab  9884  kardexOLD  9900  kardenOLD  9902  cardf2  9951  cardiun  9990  alephval3  10116  dfac3  10127  dfac5lem3  10131  dfac5lem4  10132  dfac2b  10136  kmlem12  10167  cardcf  10256  cfeq0  10261  cfsuc  10262  cff1  10263  cflim2  10268  cfss  10270  axdc3lem2  10456  axdc3lem3  10457  axdclem  10524  brdom7disj  10537  brdom6disj  10538  tskuni  10795  gruina  10830  nqpr  11026  supadd  12210  supmul  12214  dfnn2  12273  dfuzi  12715  seqof  14125  hashfacen  14521  hashf1lem1  14522  hashf1lem2  14523  0csh0  14866  trclun  15089  dfrtrcl2  15137  shftfval  15145  infcvgaux1i  15948  sursubmefmnd  19006  injsubmefmnd  19007  smndex2dnrinv  19028  symg1bas  19519  pmtrprfvalrn  19616  psgnvali  19636  efgrelexlemb  19878  lss1d  21148  lidldvgen  21566  zndvds  21763  mpfind  22332  pf1ind  22581  cmpsublem  23625  cmpsub  23626  ptpjopn  23839  ptclsg  23842  txdis1cn  23862  tx1stc  23877  hauspwpwf1  24214  qustgplem  24348  ustn0  24448  i1fadd  25924  i1fmul  25925  i1fmulc  25932  nosupno  27937  nosupbnd1lem1  27942  noinfno  27952  addsproplem2  28233  addsproplem4  28235  addsproplem5  28236  addsproplem6  28237  addsuniflem  28264  negsid  28304  mulsproplem9  28387  mulsproplem12  28390  sltmuls1  28410  sltmuls2  28411  precsexlem9  28478  precsexlem11  28480  dfn0s2  28595  recut  28757  elreno2  28758  ausgrusgri  29614  ushgredgedg  29675  ushgredgedgloop  29677  wspniunwspnon  30377  rusgrnumwwlkb0  30428  fusgr2wsp2nb  30800  nmosetn0  31232  nmoolb  31238  nmlno0lem  31260  nmopsetn0  32332  nmfnsetn0  32345  nmoplb  32374  nmfnlb  32391  nmlnop0iALT  32462  nmopun  32481  nmcexi  32493  branmfn  32572  pjnmopi  32615  fpwrelmapffslem  33190  ldlfcntref  34351  esumc  34548  orvcval2  34957  derangenlem  35737  satfrnmapom  35936  fmlaomn0  35956  fmlasucdisj  35965  dmopab3rexdif  35971  2goelgoanfmla1  35990  mclsssvlem  36128  mclsind  36136  dfon2lem3  36349  dfon2lem7  36353  fnimage  36493  imageval  36494  dfttc4  37136  poimirlem4  38360  poimirlem5  38361  poimirlem6  38362  poimirlem7  38363  poimirlem8  38364  poimirlem9  38365  poimirlem10  38366  poimirlem11  38367  poimirlem12  38368  poimirlem13  38369  poimirlem14  38370  poimirlem15  38371  poimirlem16  38372  poimirlem17  38373  poimirlem18  38374  poimirlem19  38375  poimirlem20  38376  poimirlem21  38377  poimirlem22  38378  poimirlem25  38381  poimirlem26  38382  poimirlem27  38383  poimirlem29  38385  poimirlem31  38387  mblfinlem3  38395  mblfinlem4  38396  ismblfin  38397  itg2addnc  38410  sdclem2  38479  sdclem1  38480  heibor1lem  38546  glbconxN  40238  pmapglbx  40629  dvhb1dimN  41846  sticksstones10  43008  sticksstones11  43009  sticksstones12a  43010  sticksstones12  43011  sticksstones17  43016  sticksstones18  43017  sticksstones19  43018  redvmptabs  43222  abbibw  43510  eldiophss  43606  setindtrs  43853  hbtlem2  43952  hbtlem5  43956  rngunsnply  43997  oaun3lem1  44202  oadif1lem  44207  oadif1  44208  dftrcl3  44547  brtrclfv2  44554  dfrtrcl3  44560  dfhe3  44602  cpcolld  45069  nzss  45128  upbdrech  46125  fourierdlem36  46958  sge0resplit  47221  hoidmvlelem1  47410  fsetsniunop  47924  elsprel  48362  ixpv  49803  iinfconstbas  49979  setrec2lem1  50606