Theorem elab 3558

Description: Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. (Contributed by NM, 1-Aug-1994.) Remove dependency on ax-13 2334. (Revised by Steven Nguyen, 29-Nov-2022.)

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1601   ∈ wcel 2107  {cab 2763  Vcvv 3398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400

This theorem is referenced by:  ralab  3577  rexab  3579  intab  4740  dfiin2g  4786  dfiunv2  4789  opeliunxp  5416  elabrex  6773  abrexco  6774  uniuni  7248  finds  7370  finds2  7372  funcnvuni  7398  fun11iun  7405  mapval2  8170  sbthlem2  8359  ssenen  8422  dffi2  8617  dffi3  8625  tctr  8913  tcmin  8914  tc2  8915  tz9.13  8951  tcrank  9044  kardex  9054  karden  9055  cardf2  9102  cardiun  9141  alephval3  9266  dfac3  9277  dfac5lem3  9281  dfac5lem4  9282  dfac2b  9286  dfac2OLD  9288  kmlem12  9318  cardcf  9409  cfeq0  9413  cfsuc  9414  cff1  9415  cflim2  9420  cfss  9422  axdc3lem2  9608  axdc3lem3  9609  axdclem  9676  brdom7disj  9688  brdom6disj  9689  tskuni  9940  gruina  9975  nqpr  10171  supadd  11345  supmul  11349  dfnn2  11389  dfuzi  11820  seqof  13176  hashfacen  13552  hashf1lem1  13553  hashf1lem2  13554  0csh0  13943  0csh0OLD  13944  trclun  14162  dfrtrcl2  14209  shftfval  14217  infcvgaux1i  14993  symg1bas  18199  pmtrprfvalrn  18291  psgnvali  18312  efgrelexlemb  18549  lss1d  19358  lidldvgen  19652  mpfind  19932  pf1ind  20115  zndvds  20293  cmpsublem  21611  cmpsub  21612  ptpjopn  21824  ptclsg  21827  txdis1cn  21847  tx1stc  21862  hauspwpwf1  22199  qustgplem  22332  ustn0  22432  i1fadd  23899  i1fmul  23900  i1fmulc  23907  ausgrusgri  26517  ushgredgedg  26575  ushgredgedgloop  26577  ushgredgedgloopOLD  26578  wspniunwspnon  27303  rusgrnumwwlkb0  27351  fusgr2wsp2nb  27742  nmosetn0  28192  nmoolb  28198  nmlno0lem  28220  nmopsetn0  29296  nmfnsetn0  29309  nmoplb  29338  nmfnlb  29355  nmlnop0iALT  29426  nmopun  29445  nmcexi  29457  branmfn  29536  pjnmopi  29579  fpwrelmapffslem  30073  ldlfcntref  30519  esumc  30711  orvcval2  31119  derangenlem  31752  mclsssvlem  32058  mclsind  32066  dfon2lem3  32278  dfon2lem7  32282  nosupno  32438  nosupbnd1lem1  32443  fnimage  32625  imageval  32626  poimirlem4  34041  poimirlem5  34042  poimirlem6  34043  poimirlem7  34044  poimirlem8  34045  poimirlem9  34046  poimirlem10  34047  poimirlem11  34048  poimirlem12  34049  poimirlem13  34050  poimirlem14  34051  poimirlem15  34052  poimirlem16  34053  poimirlem17  34054  poimirlem18  34055  poimirlem19  34056  poimirlem20  34057  poimirlem21  34058  poimirlem22  34059  poimirlem25  34062  poimirlem26  34063  poimirlem27  34064  poimirlem29  34066  poimirlem31  34068  mblfinlem3  34076  mblfinlem4  34077  ismblfin  34078  itg2addnc  34091  sdclem2  34164  sdclem1  34165  heibor1lem  34234  glbconxN  35534  pmapglbx  35925  dvhb1dimN  37142  eldiophss  38302  setindtrs  38555  hbtlem2  38657  hbtlem5  38661  rngunsnply  38706  dftrcl3  38973  brtrclfv2  38980  dfrtrcl3  38986  dfhe3  39029  nzss  39476  upbdrech  40432  fourierdlem36  41291  sge0resplit  41551  hoidmvlelem1  41740  elsprel  42418  opeliun2xp  43130  setrec2lem1  43549