Theorem elab 3668

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106  {cab 2709  Vcvv 3474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810

This theorem is referenced by:  ralabOLD  3688  rexabOLD  3691  intab  4982  dfiun2g  5033  dfiin2g  5035  dfiunv2  5038  opeliunxp  5743  dmopab2rex  5917  iotanul2  6513  elabrex  7241  abrexco  7242  uniuni  7748  finds  7888  finds2  7890  funcnvuni  7921  fiunlem  7927  fiun  7928  f1iun  7929  mapfset  8843  mapfoss  8845  fsetsspwxp  8846  mapval2  8865  sbthlem2  9083  ssenen  9150  dffi2  9417  dffi3  9425  tctr  9734  tcmin  9735  tc2  9736  tz9.13  9785  tcrank  9878  kardex  9888  karden  9889  cardf2  9937  cardiun  9976  alephval3  10104  dfac3  10115  dfac5lem3  10119  dfac5lem4  10120  dfac2b  10124  kmlem12  10155  cardcf  10246  cfeq0  10250  cfsuc  10251  cff1  10252  cflim2  10257  cfss  10259  axdc3lem2  10445  axdc3lem3  10446  axdclem  10513  brdom7disj  10525  brdom6disj  10526  tskuni  10777  gruina  10812  nqpr  11008  supadd  12181  supmul  12185  dfnn2  12224  dfuzi  12652  seqof  14024  hashfacen  14412  hashfacenOLD  14413  hashf1lem1  14414  hashf1lem1OLD  14415  hashf1lem2  14416  0csh0  14742  trclun  14960  dfrtrcl2  15008  shftfval  15016  infcvgaux1i  15802  sursubmefmnd  18776  injsubmefmnd  18777  smndex2dnrinv  18795  symg1bas  19257  pmtrprfvalrn  19355  psgnvali  19375  efgrelexlemb  19617  lss1d  20573  lidldvgen  20892  zndvds  21104  mpfind  21669  pf1ind  21873  cmpsublem  22902  cmpsub  22903  ptpjopn  23115  ptclsg  23118  txdis1cn  23138  tx1stc  23153  hauspwpwf1  23490  qustgplem  23624  ustn0  23724  i1fadd  25211  i1fmul  25212  i1fmulc  25220  nosupno  27203  nosupbnd1lem1  27208  noinfno  27218  addsproplem2  27451  addsproplem4  27453  addsproplem5  27454  addsproplem6  27455  addsuniflem  27481  negsid  27512  mulsproplem9  27577  mulsproplem12  27580  ssltmul1  27599  ssltmul2  27600  precsexlem9  27658  precsexlem11  27660  ausgrusgri  28425  ushgredgedg  28483  ushgredgedgloop  28485  wspniunwspnon  29174  rusgrnumwwlkb0  29222  fusgr2wsp2nb  29584  nmosetn0  30013  nmoolb  30019  nmlno0lem  30041  nmopsetn0  31113  nmfnsetn0  31126  nmoplb  31155  nmfnlb  31172  nmlnop0iALT  31243  nmopun  31262  nmcexi  31274  branmfn  31353  pjnmopi  31396  fpwrelmapffslem  31952  ldlfcntref  32829  esumc  33044  orvcval2  33452  derangenlem  34157  satfrnmapom  34356  fmlaomn0  34376  fmlasucdisj  34385  dmopab3rexdif  34391  2goelgoanfmla1  34410  mclsssvlem  34548  mclsind  34556  dfon2lem3  34752  dfon2lem7  34756  fnimage  34896  imageval  34897  poimirlem4  36487  poimirlem5  36488  poimirlem6  36489  poimirlem7  36490  poimirlem8  36491  poimirlem9  36492  poimirlem10  36493  poimirlem11  36494  poimirlem12  36495  poimirlem13  36496  poimirlem14  36497  poimirlem15  36498  poimirlem16  36499  poimirlem17  36500  poimirlem18  36501  poimirlem19  36502  poimirlem20  36503  poimirlem21  36504  poimirlem22  36505  poimirlem25  36508  poimirlem26  36509  poimirlem27  36510  poimirlem29  36512  poimirlem31  36514  mblfinlem3  36522  mblfinlem4  36523  ismblfin  36524  itg2addnc  36537  sdclem2  36605  sdclem1  36606  heibor1lem  36672  glbconxN  38244  pmapglbx  38635  dvhb1dimN  39852  sticksstones10  40966  sticksstones11  40967  sticksstones12a  40968  sticksstones12  40969  sticksstones17  40974  sticksstones18  40975  sticksstones19  40976  eldiophss  41502  setindtrs  41754  hbtlem2  41856  hbtlem5  41860  rngunsnply  41905  oaun3lem1  42114  oadif1lem  42119  oadif1  42120  dftrcl3  42461  brtrclfv2  42468  dfrtrcl3  42474  dfhe3  42516  elscottab  42993  cpcolld  43007  nzss  43066  upbdrech  44005  fourierdlem36  44849  sge0resplit  45112  hoidmvlelem1  45301  fsetsniunop  45749  elsprel  46133  opeliun2xp  46998  setrec2lem1  47728