Theorem elab 3694

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2108  {cab 2717  Vcvv 3488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819

This theorem is referenced by:  ralabOLD  3714  rexabOLD  3717  intab  5002  dfiun2g  5053  dfiin2g  5055  dfiunv2  5058  opeliunxp  5767  dmopab2rex  5942  iotanul2  6543  elabrex  7279  abrexco  7281  uniuni  7797  finds  7936  finds2  7938  funcnvuni  7972  fiunlem  7982  fiun  7983  f1iun  7984  mapfset  8908  mapfoss  8910  fsetsspwxp  8911  mapval2  8930  sbthlem2  9150  ssenen  9217  dffi2  9492  dffi3  9500  tctr  9809  tcmin  9810  tc2  9811  tz9.13  9860  tcrank  9953  kardex  9963  karden  9964  cardf2  10012  cardiun  10051  alephval3  10179  dfac3  10190  dfac5lem3  10194  dfac5lem4  10195  dfac5lem4OLD  10197  dfac2b  10200  kmlem12  10231  cardcf  10321  cfeq0  10325  cfsuc  10326  cff1  10327  cflim2  10332  cfss  10334  axdc3lem2  10520  axdc3lem3  10521  axdclem  10588  brdom7disj  10600  brdom6disj  10601  tskuni  10852  gruina  10887  nqpr  11083  supadd  12263  supmul  12267  dfnn2  12306  dfuzi  12734  seqof  14110  hashfacen  14503  hashf1lem1  14504  hashf1lem2  14505  0csh0  14841  trclun  15063  dfrtrcl2  15111  shftfval  15119  infcvgaux1i  15905  sursubmefmnd  18931  injsubmefmnd  18932  smndex2dnrinv  18950  symg1bas  19432  pmtrprfvalrn  19530  psgnvali  19550  efgrelexlemb  19792  lss1d  20984  lidldvgen  21367  zndvds  21591  mpfind  22154  pf1ind  22380  cmpsublem  23428  cmpsub  23429  ptpjopn  23641  ptclsg  23644  txdis1cn  23664  tx1stc  23679  hauspwpwf1  24016  qustgplem  24150  ustn0  24250  i1fadd  25749  i1fmul  25750  i1fmulc  25758  nosupno  27766  nosupbnd1lem1  27771  noinfno  27781  addsproplem2  28021  addsproplem4  28023  addsproplem5  28024  addsproplem6  28025  addsuniflem  28052  negsid  28091  mulsproplem9  28168  mulsproplem12  28171  ssltmul1  28191  ssltmul2  28192  precsexlem9  28257  precsexlem11  28259  dfn0s2  28354  recut  28446  0reno  28447  ausgrusgri  29203  ushgredgedg  29264  ushgredgedgloop  29266  wspniunwspnon  29956  rusgrnumwwlkb0  30004  fusgr2wsp2nb  30366  nmosetn0  30797  nmoolb  30803  nmlno0lem  30825  nmopsetn0  31897  nmfnsetn0  31910  nmoplb  31939  nmfnlb  31956  nmlnop0iALT  32027  nmopun  32046  nmcexi  32058  branmfn  32137  pjnmopi  32180  fpwrelmapffslem  32746  ldlfcntref  33800  esumc  34015  orvcval2  34423  derangenlem  35139  satfrnmapom  35338  fmlaomn0  35358  fmlasucdisj  35367  dmopab3rexdif  35373  2goelgoanfmla1  35392  mclsssvlem  35530  mclsind  35538  dfon2lem3  35749  dfon2lem7  35753  fnimage  35893  imageval  35894  poimirlem4  37584  poimirlem5  37585  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem9  37589  poimirlem10  37590  poimirlem11  37591  poimirlem12  37592  poimirlem13  37593  poimirlem14  37594  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem18  37598  poimirlem19  37599  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem25  37605  poimirlem26  37606  poimirlem27  37607  poimirlem29  37609  poimirlem31  37611  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  itg2addnc  37634  sdclem2  37702  sdclem1  37703  heibor1lem  37769  glbconxN  39335  pmapglbx  39726  dvhb1dimN  40943  sticksstones10  42112  sticksstones11  42113  sticksstones12a  42114  sticksstones12  42115  sticksstones17  42120  sticksstones18  42121  sticksstones19  42122  abbibw  42632  eldiophss  42730  setindtrs  42982  hbtlem2  43081  hbtlem5  43085  rngunsnply  43130  oaun3lem1  43336  oadif1lem  43341  oadif1  43342  dftrcl3  43682  brtrclfv2  43689  dfrtrcl3  43695  dfhe3  43737  elscottab  44213  cpcolld  44227  nzss  44286  upbdrech  45220  fourierdlem36  46064  sge0resplit  46327  hoidmvlelem1  46516  fsetsniunop  46964  elsprel  47349  opeliun2xp  48057  setrec2lem1  48785