Theorem elab 3639

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1561   ∈ wcel 2143  {cab 2741  Vcvv 3455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1564  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838

This theorem is referenced by:  intab  4937  dfiun2g  4988  dfiin2g  4989  dfiunv2  4992  opeliunxp  5715  opeliun2xp  5716  dmopab2rex  5894  iotanul2  6494  elabrex  7226  abrexco  7228  uniuni  7745  finds  7877  finds2  7879  funcnvuni  7913  fiunlem  7923  fiun  7924  f1iun  7925  mapfset  8831  mapfoss  8833  fsetsspwxp  8834  mapval2  8854  sbthlem2  9060  ssenen  9123  dffi2  9367  dffi3  9375  tctr  9691  tcmin  9692  tc2  9693  tz9.13  9747  tcrank  9840  elscottab  9854  kardex  9864  karden  9865  cardf2  9913  cardiun  9952  alephval3  10078  dfac3  10089  dfac5lem3  10093  dfac5lem4  10094  dfac2b  10098  kmlem12  10129  cardcf  10219  cfeq0  10224  cfsuc  10225  cff1  10226  cflim2  10231  cfss  10233  axdc3lem2  10419  axdc3lem3  10420  axdclem  10487  brdom7disj  10499  brdom6disj  10500  tskuni  10752  gruina  10787  nqpr  10983  supadd  12170  supmul  12174  dfnn2  12233  dfuzi  12674  seqof  14082  hashfacen  14477  hashf1lem1  14478  hashf1lem2  14479  0csh0  14816  trclun  15037  dfrtrcl2  15085  shftfval  15093  infcvgaux1i  15897  sursubmefmnd  18940  injsubmefmnd  18941  smndex2dnrinv  18962  symg1bas  19441  pmtrprfvalrn  19538  psgnvali  19558  efgrelexlemb  19800  lss1d  21037  lidldvgen  21411  zndvds  21608  mpfind  22175  pf1ind  22425  cmpsublem  23466  cmpsub  23467  ptpjopn  23679  ptclsg  23682  txdis1cn  23702  tx1stc  23717  hauspwpwf1  24054  qustgplem  24188  ustn0  24288  i1fadd  25764  i1fmul  25765  i1fmulc  25772  nosupno  27774  nosupbnd1lem1  27779  noinfno  27789  addsproplem2  28070  addsproplem4  28072  addsproplem5  28073  addsproplem6  28074  addsuniflem  28101  negsid  28141  mulsproplem9  28224  mulsproplem12  28227  sltmuls1  28247  sltmuls2  28248  precsexlem9  28315  precsexlem11  28317  dfn0s2  28432  recut  28594  elreno2  28595  ausgrusgri  29376  ushgredgedg  29437  ushgredgedgloop  29439  wspniunwspnon  30130  rusgrnumwwlkb0  30181  fusgr2wsp2nb  30543  nmosetn0  30975  nmoolb  30981  nmlno0lem  31003  nmopsetn0  32075  nmfnsetn0  32088  nmoplb  32117  nmfnlb  32134  nmlnop0iALT  32205  nmopun  32224  nmcexi  32236  branmfn  32315  pjnmopi  32358  fpwrelmapffslem  32940  ldlfcntref  34153  esumc  34350  orvcval2  34758  derangenlem  35526  satfrnmapom  35725  fmlaomn0  35745  fmlasucdisj  35754  dmopab3rexdif  35760  2goelgoanfmla1  35779  mclsssvlem  35917  mclsind  35925  dfon2lem3  36138  dfon2lem7  36142  fnimage  36282  imageval  36283  dfttc4  36895  poimirlem4  38128  poimirlem5  38129  poimirlem6  38130  poimirlem7  38131  poimirlem8  38132  poimirlem9  38133  poimirlem10  38134  poimirlem11  38135  poimirlem12  38136  poimirlem13  38137  poimirlem14  38138  poimirlem15  38139  poimirlem16  38140  poimirlem17  38141  poimirlem18  38142  poimirlem19  38143  poimirlem20  38144  poimirlem21  38145  poimirlem22  38146  poimirlem25  38149  poimirlem26  38150  poimirlem27  38151  poimirlem29  38153  poimirlem31  38155  mblfinlem3  38163  mblfinlem4  38164  ismblfin  38165  itg2addnc  38178  sdclem2  38246  sdclem1  38247  heibor1lem  38313  glbconxN  40007  pmapglbx  40398  dvhb1dimN  41615  sticksstones10  42777  sticksstones11  42778  sticksstones12a  42779  sticksstones12  42780  sticksstones17  42785  sticksstones18  42786  sticksstones19  42787  redvmptabs  42974  abbibw  43264  eldiophss  43360  setindtrs  43607  hbtlem2  43706  hbtlem5  43710  rngunsnply  43751  oaun3lem1  43956  oadif1lem  43961  oadif1  43962  dftrcl3  44301  brtrclfv2  44308  dfrtrcl3  44314  dfhe3  44356  cpcolld  44825  nzss  44884  upbdrech  45875  fourierdlem36  46708  sge0resplit  46971  hoidmvlelem1  47160  fsetsniunop  47634  elsprel  48072  ixpv  49502  iinfconstbas  49678  setrec2lem1  50305