Theorem elab 3619

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540   ∈ wcel 2105  {cab 2713  Vcvv 3441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814

This theorem is referenced by:  ralabOLD  3639  rexabOLD  3642  intab  4926  dfiun2g  4977  dfiin2g  4979  dfiunv2  4982  opeliunxp  5685  dmopab2rex  5859  iotanul2  6449  elabrex  7172  abrexco  7173  uniuni  7674  finds  7813  finds2  7815  funcnvuni  7846  fiunlem  7852  fiun  7853  f1iun  7854  mapfset  8709  mapfoss  8711  fsetsspwxp  8712  mapval2  8731  sbthlem2  8949  ssenen  9016  dffi2  9280  dffi3  9288  tctr  9597  tcmin  9598  tc2  9599  tz9.13  9648  tcrank  9741  kardex  9751  karden  9752  cardf2  9800  cardiun  9839  alephval3  9967  dfac3  9978  dfac5lem3  9982  dfac5lem4  9983  dfac2b  9987  kmlem12  10018  cardcf  10109  cfeq0  10113  cfsuc  10114  cff1  10115  cflim2  10120  cfss  10122  axdc3lem2  10308  axdc3lem3  10309  axdclem  10376  brdom7disj  10388  brdom6disj  10389  tskuni  10640  gruina  10675  nqpr  10871  supadd  12044  supmul  12048  dfnn2  12087  dfuzi  12512  seqof  13881  hashfacen  14266  hashfacenOLD  14267  hashf1lem1  14268  hashf1lem1OLD  14269  hashf1lem2  14270  0csh0  14604  trclun  14824  dfrtrcl2  14872  shftfval  14880  infcvgaux1i  15668  sursubmefmnd  18631  injsubmefmnd  18632  smndex2dnrinv  18650  symg1bas  19094  pmtrprfvalrn  19192  psgnvali  19212  efgrelexlemb  19451  lss1d  20331  lidldvgen  20632  zndvds  20863  mpfind  21423  pf1ind  21627  cmpsublem  22656  cmpsub  22657  ptpjopn  22869  ptclsg  22872  txdis1cn  22892  tx1stc  22907  hauspwpwf1  23244  qustgplem  23378  ustn0  23478  i1fadd  24965  i1fmul  24966  i1fmulc  24974  nosupno  26957  nosupbnd1lem1  26962  noinfno  26972  ausgrusgri  27827  ushgredgedg  27885  ushgredgedgloop  27887  wspniunwspnon  28576  rusgrnumwwlkb0  28624  fusgr2wsp2nb  28986  nmosetn0  29415  nmoolb  29421  nmlno0lem  29443  nmopsetn0  30515  nmfnsetn0  30528  nmoplb  30557  nmfnlb  30574  nmlnop0iALT  30645  nmopun  30664  nmcexi  30676  branmfn  30755  pjnmopi  30798  fpwrelmapffslem  31354  ldlfcntref  32102  esumc  32317  orvcval2  32725  derangenlem  33432  satfrnmapom  33631  fmlaomn0  33651  fmlasucdisj  33660  dmopab3rexdif  33666  2goelgoanfmla1  33685  mclsssvlem  33823  mclsind  33831  dfon2lem3  34044  dfon2lem7  34048  fnimage  34327  imageval  34328  poimirlem4  35894  poimirlem5  35895  poimirlem6  35896  poimirlem7  35897  poimirlem8  35898  poimirlem9  35899  poimirlem10  35900  poimirlem11  35901  poimirlem12  35902  poimirlem13  35903  poimirlem14  35904  poimirlem15  35905  poimirlem16  35906  poimirlem17  35907  poimirlem18  35908  poimirlem19  35909  poimirlem20  35910  poimirlem21  35911  poimirlem22  35912  poimirlem25  35915  poimirlem26  35916  poimirlem27  35917  poimirlem29  35919  poimirlem31  35921  mblfinlem3  35929  mblfinlem4  35930  ismblfin  35931  itg2addnc  35944  sdclem2  36013  sdclem1  36014  heibor1lem  36080  glbconxN  37654  pmapglbx  38045  dvhb1dimN  39262  sticksstones10  40376  sticksstones11  40377  sticksstones12a  40378  sticksstones12  40379  sticksstones17  40384  sticksstones18  40385  sticksstones19  40386  mhphf  40553  eldiophss  40866  setindtrs  41118  hbtlem2  41220  hbtlem5  41224  rngunsnply  41269  dftrcl3  41657  brtrclfv2  41664  dfrtrcl3  41670  dfhe3  41712  elscottab  42191  cpcolld  42205  nzss  42264  upbdrech  43187  fourierdlem36  44028  sge0resplit  44289  hoidmvlelem1  44478  fsetsniunop  44902  elsprel  45286  opeliun2xp  46027  setrec2lem1  46758