Theorem elab 3636

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {cab 2715  Vcvv 3442

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812

This theorem is referenced by:  intab  4935  dfiun2g  4987  dfiin2g  4988  dfiunv2  4991  opeliunxp  5701  opeliun2xp  5702  dmopab2rex  5876  iotanul2  6475  elabrex  7200  abrexco  7202  uniuni  7719  finds  7850  finds2  7852  funcnvuni  7886  fiunlem  7898  fiun  7899  f1iun  7900  mapfset  8801  mapfoss  8803  fsetsspwxp  8804  mapval2  8824  sbthlem2  9030  ssenen  9093  dffi2  9340  dffi3  9348  tctr  9661  tcmin  9662  tc2  9663  tz9.13  9717  tcrank  9810  kardex  9820  karden  9821  cardf2  9869  cardiun  9908  alephval3  10034  dfac3  10045  dfac5lem3  10049  dfac5lem4  10050  dfac5lem4OLD  10052  dfac2b  10055  kmlem12  10086  cardcf  10176  cfeq0  10180  cfsuc  10181  cff1  10182  cflim2  10187  cfss  10189  axdc3lem2  10375  axdc3lem3  10376  axdclem  10443  brdom7disj  10455  brdom6disj  10456  tskuni  10708  gruina  10743  nqpr  10939  supadd  12124  supmul  12128  dfnn2  12172  dfuzi  12597  seqof  13996  hashfacen  14391  hashf1lem1  14392  hashf1lem2  14393  0csh0  14730  trclun  14951  dfrtrcl2  14999  shftfval  15007  infcvgaux1i  15794  sursubmefmnd  18835  injsubmefmnd  18836  smndex2dnrinv  18857  symg1bas  19337  pmtrprfvalrn  19434  psgnvali  19454  efgrelexlemb  19696  lss1d  20931  lidldvgen  21306  zndvds  21521  mpfind  22087  pf1ind  22316  cmpsublem  23360  cmpsub  23361  ptpjopn  23573  ptclsg  23576  txdis1cn  23596  tx1stc  23611  hauspwpwf1  23948  qustgplem  24082  ustn0  24182  i1fadd  25669  i1fmul  25670  i1fmulc  25677  nosupno  27688  nosupbnd1lem1  27693  noinfno  27703  addsproplem2  27983  addsproplem4  27985  addsproplem5  27986  addsproplem6  27987  addsuniflem  28014  negsid  28054  mulsproplem9  28137  mulsproplem12  28140  sltmuls1  28160  sltmuls2  28161  precsexlem9  28228  precsexlem11  28230  dfn0s2  28345  recut  28507  elreno2  28508  ausgrusgri  29259  ushgredgedg  29320  ushgredgedgloop  29322  wspniunwspnon  30014  rusgrnumwwlkb0  30065  fusgr2wsp2nb  30427  nmosetn0  30859  nmoolb  30865  nmlno0lem  30887  nmopsetn0  31959  nmfnsetn0  31972  nmoplb  32001  nmfnlb  32018  nmlnop0iALT  32089  nmopun  32108  nmcexi  32120  branmfn  32199  pjnmopi  32242  fpwrelmapffslem  32828  ldlfcntref  34038  esumc  34235  orvcval2  34643  derangenlem  35393  satfrnmapom  35592  fmlaomn0  35612  fmlasucdisj  35621  dmopab3rexdif  35627  2goelgoanfmla1  35646  mclsssvlem  35784  mclsind  35792  dfon2lem3  36005  dfon2lem7  36009  fnimage  36149  imageval  36150  poimirlem4  37904  poimirlem5  37905  poimirlem6  37906  poimirlem7  37907  poimirlem8  37908  poimirlem9  37909  poimirlem10  37910  poimirlem11  37911  poimirlem12  37912  poimirlem13  37913  poimirlem14  37914  poimirlem15  37915  poimirlem16  37916  poimirlem17  37917  poimirlem18  37918  poimirlem19  37919  poimirlem20  37920  poimirlem21  37921  poimirlem22  37922  poimirlem25  37925  poimirlem26  37926  poimirlem27  37927  poimirlem29  37929  poimirlem31  37931  mblfinlem3  37939  mblfinlem4  37940  ismblfin  37941  itg2addnc  37954  sdclem2  38022  sdclem1  38023  heibor1lem  38089  glbconxN  39783  pmapglbx  40174  dvhb1dimN  41391  sticksstones10  42554  sticksstones11  42555  sticksstones12a  42556  sticksstones12  42557  sticksstones17  42562  sticksstones18  42563  sticksstones19  42564  redvmptabs  42759  abbibw  43064  eldiophss  43160  setindtrs  43411  hbtlem2  43510  hbtlem5  43514  rngunsnply  43555  oaun3lem1  43760  oadif1lem  43765  oadif1  43766  dftrcl3  44105  brtrclfv2  44112  dfrtrcl3  44118  dfhe3  44160  elscottab  44629  cpcolld  44643  nzss  44702  upbdrech  45696  fourierdlem36  46530  sge0resplit  46793  hoidmvlelem1  46982  fsetsniunop  47438  elsprel  47864  ixpv  49278  iinfconstbas  49454  setrec2lem1  50081