Theorem elab 3669

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ∈ wcel 2107  {cab 2710  Vcvv 3475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811

This theorem is referenced by:  ralabOLD  3689  rexabOLD  3692  intab  4983  dfiun2g  5034  dfiin2g  5036  dfiunv2  5039  opeliunxp  5744  dmopab2rex  5918  iotanul2  6514  elabrex  7242  abrexco  7243  uniuni  7749  finds  7889  finds2  7891  funcnvuni  7922  fiunlem  7928  fiun  7929  f1iun  7930  mapfset  8844  mapfoss  8846  fsetsspwxp  8847  mapval2  8866  sbthlem2  9084  ssenen  9151  dffi2  9418  dffi3  9426  tctr  9735  tcmin  9736  tc2  9737  tz9.13  9786  tcrank  9879  kardex  9889  karden  9890  cardf2  9938  cardiun  9977  alephval3  10105  dfac3  10116  dfac5lem3  10120  dfac5lem4  10121  dfac2b  10125  kmlem12  10156  cardcf  10247  cfeq0  10251  cfsuc  10252  cff1  10253  cflim2  10258  cfss  10260  axdc3lem2  10446  axdc3lem3  10447  axdclem  10514  brdom7disj  10526  brdom6disj  10527  tskuni  10778  gruina  10813  nqpr  11009  supadd  12182  supmul  12186  dfnn2  12225  dfuzi  12653  seqof  14025  hashfacen  14413  hashfacenOLD  14414  hashf1lem1  14415  hashf1lem1OLD  14416  hashf1lem2  14417  0csh0  14743  trclun  14961  dfrtrcl2  15009  shftfval  15017  infcvgaux1i  15803  sursubmefmnd  18777  injsubmefmnd  18778  smndex2dnrinv  18796  symg1bas  19258  pmtrprfvalrn  19356  psgnvali  19376  efgrelexlemb  19618  lss1d  20574  lidldvgen  20893  zndvds  21105  mpfind  21670  pf1ind  21874  cmpsublem  22903  cmpsub  22904  ptpjopn  23116  ptclsg  23119  txdis1cn  23139  tx1stc  23154  hauspwpwf1  23491  qustgplem  23625  ustn0  23725  i1fadd  25212  i1fmul  25213  i1fmulc  25221  nosupno  27206  nosupbnd1lem1  27211  noinfno  27221  addsproplem2  27454  addsproplem4  27456  addsproplem5  27457  addsproplem6  27458  addsuniflem  27484  negsid  27515  mulsproplem9  27580  mulsproplem12  27583  ssltmul1  27602  ssltmul2  27603  precsexlem9  27661  precsexlem11  27663  ausgrusgri  28428  ushgredgedg  28486  ushgredgedgloop  28488  wspniunwspnon  29177  rusgrnumwwlkb0  29225  fusgr2wsp2nb  29587  nmosetn0  30018  nmoolb  30024  nmlno0lem  30046  nmopsetn0  31118  nmfnsetn0  31131  nmoplb  31160  nmfnlb  31177  nmlnop0iALT  31248  nmopun  31267  nmcexi  31279  branmfn  31358  pjnmopi  31401  fpwrelmapffslem  31957  ldlfcntref  32834  esumc  33049  orvcval2  33457  derangenlem  34162  satfrnmapom  34361  fmlaomn0  34381  fmlasucdisj  34390  dmopab3rexdif  34396  2goelgoanfmla1  34415  mclsssvlem  34553  mclsind  34561  dfon2lem3  34757  dfon2lem7  34761  fnimage  34901  imageval  34902  poimirlem4  36492  poimirlem5  36493  poimirlem6  36494  poimirlem7  36495  poimirlem8  36496  poimirlem9  36497  poimirlem10  36498  poimirlem11  36499  poimirlem12  36500  poimirlem13  36501  poimirlem14  36502  poimirlem15  36503  poimirlem16  36504  poimirlem17  36505  poimirlem18  36506  poimirlem19  36507  poimirlem20  36508  poimirlem21  36509  poimirlem22  36510  poimirlem25  36513  poimirlem26  36514  poimirlem27  36515  poimirlem29  36517  poimirlem31  36519  mblfinlem3  36527  mblfinlem4  36528  ismblfin  36529  itg2addnc  36542  sdclem2  36610  sdclem1  36611  heibor1lem  36677  glbconxN  38249  pmapglbx  38640  dvhb1dimN  39857  sticksstones10  40971  sticksstones11  40972  sticksstones12a  40973  sticksstones12  40974  sticksstones17  40979  sticksstones18  40980  sticksstones19  40981  eldiophss  41512  setindtrs  41764  hbtlem2  41866  hbtlem5  41870  rngunsnply  41915  oaun3lem1  42124  oadif1lem  42129  oadif1  42130  dftrcl3  42471  brtrclfv2  42478  dfrtrcl3  42484  dfhe3  42526  elscottab  43003  cpcolld  43017  nzss  43076  upbdrech  44015  fourierdlem36  44859  sge0resplit  45122  hoidmvlelem1  45311  fsetsniunop  45759  elsprel  46143  opeliun2xp  47008  setrec2lem1  47738