Theorem elab 3609

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2106  {cab 2715  Vcvv 3432

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816

This theorem is referenced by:  ralabOLD  3629  rexabOLD  3632  intab  4909  dfiun2g  4960  dfiin2g  4962  dfiunv2  4965  opeliunxp  5654  dmopab2rex  5826  elabrex  7116  abrexco  7117  uniuni  7612  finds  7745  finds2  7747  funcnvuni  7778  fiunlem  7784  fiun  7785  f1iun  7786  mapfset  8638  mapfoss  8640  fsetsspwxp  8641  mapval2  8660  sbthlem2  8871  ssenen  8938  dffi2  9182  dffi3  9190  tctr  9498  tcmin  9499  tc2  9500  tz9.13  9549  tcrank  9642  kardex  9652  karden  9653  cardf2  9701  cardiun  9740  alephval3  9866  dfac3  9877  dfac5lem3  9881  dfac5lem4  9882  dfac2b  9886  kmlem12  9917  cardcf  10008  cfeq0  10012  cfsuc  10013  cff1  10014  cflim2  10019  cfss  10021  axdc3lem2  10207  axdc3lem3  10208  axdclem  10275  brdom7disj  10287  brdom6disj  10288  tskuni  10539  gruina  10574  nqpr  10770  supadd  11943  supmul  11947  dfnn2  11986  dfuzi  12411  seqof  13780  hashfacen  14166  hashfacenOLD  14167  hashf1lem1  14168  hashf1lem1OLD  14169  hashf1lem2  14170  0csh0  14506  trclun  14725  dfrtrcl2  14773  shftfval  14781  infcvgaux1i  15569  sursubmefmnd  18535  injsubmefmnd  18536  smndex2dnrinv  18554  symg1bas  18998  pmtrprfvalrn  19096  psgnvali  19116  efgrelexlemb  19356  lss1d  20225  lidldvgen  20526  zndvds  20757  mpfind  21317  pf1ind  21521  cmpsublem  22550  cmpsub  22551  ptpjopn  22763  ptclsg  22766  txdis1cn  22786  tx1stc  22801  hauspwpwf1  23138  qustgplem  23272  ustn0  23372  i1fadd  24859  i1fmul  24860  i1fmulc  24868  ausgrusgri  27538  ushgredgedg  27596  ushgredgedgloop  27598  wspniunwspnon  28288  rusgrnumwwlkb0  28336  fusgr2wsp2nb  28698  nmosetn0  29127  nmoolb  29133  nmlno0lem  29155  nmopsetn0  30227  nmfnsetn0  30240  nmoplb  30269  nmfnlb  30286  nmlnop0iALT  30357  nmopun  30376  nmcexi  30388  branmfn  30467  pjnmopi  30510  fpwrelmapffslem  31067  ldlfcntref  31804  esumc  32019  orvcval2  32425  derangenlem  33133  satfrnmapom  33332  fmlaomn0  33352  fmlasucdisj  33361  dmopab3rexdif  33367  2goelgoanfmla1  33386  mclsssvlem  33524  mclsind  33532  dfon2lem3  33761  dfon2lem7  33765  nosupno  33906  nosupbnd1lem1  33911  noinfno  33921  fnimage  34231  imageval  34232  poimirlem4  35781  poimirlem5  35782  poimirlem6  35783  poimirlem7  35784  poimirlem8  35785  poimirlem9  35786  poimirlem10  35787  poimirlem11  35788  poimirlem12  35789  poimirlem13  35790  poimirlem14  35791  poimirlem15  35792  poimirlem16  35793  poimirlem17  35794  poimirlem18  35795  poimirlem19  35796  poimirlem20  35797  poimirlem21  35798  poimirlem22  35799  poimirlem25  35802  poimirlem26  35803  poimirlem27  35804  poimirlem29  35806  poimirlem31  35808  mblfinlem3  35816  mblfinlem4  35817  ismblfin  35818  itg2addnc  35831  sdclem2  35900  sdclem1  35901  heibor1lem  35967  glbconxN  37392  pmapglbx  37783  dvhb1dimN  39000  sticksstones10  40111  sticksstones11  40112  sticksstones12a  40113  sticksstones12  40114  sticksstones17  40119  sticksstones18  40120  sticksstones19  40121  sn-iotanul  40194  mhphf  40285  eldiophss  40596  setindtrs  40847  hbtlem2  40949  hbtlem5  40953  rngunsnply  40998  dftrcl3  41328  brtrclfv2  41335  dfrtrcl3  41341  dfhe3  41383  elscottab  41862  cpcolld  41876  nzss  41935  upbdrech  42844  fourierdlem36  43684  sge0resplit  43944  hoidmvlelem1  44133  fsetsniunop  44543  elsprel  44927  opeliun2xp  45668  setrec2lem1  46399