Theorem elab 3602

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817

This theorem is referenced by:  ralabOLD  3622  rexabOLD  3625  intab  4906  dfiin2g  4958  dfiunv2  4961  opeliunxp  5645  dmopab2rex  5815  elabrex  7098  abrexco  7099  uniuni  7590  finds  7719  finds2  7721  funcnvuni  7752  fiunlem  7758  fiun  7759  f1iun  7760  mapfset  8596  mapfoss  8598  fsetsspwxp  8599  mapval2  8618  sbthlem2  8824  ssenen  8887  dffi2  9112  dffi3  9120  tctr  9429  tcmin  9430  tc2  9431  tz9.13  9480  tcrank  9573  kardex  9583  karden  9584  cardf2  9632  cardiun  9671  alephval3  9797  dfac3  9808  dfac5lem3  9812  dfac5lem4  9813  dfac2b  9817  kmlem12  9848  cardcf  9939  cfeq0  9943  cfsuc  9944  cff1  9945  cflim2  9950  cfss  9952  axdc3lem2  10138  axdc3lem3  10139  axdclem  10206  brdom7disj  10218  brdom6disj  10219  tskuni  10470  gruina  10505  nqpr  10701  supadd  11873  supmul  11877  dfnn2  11916  dfuzi  12341  seqof  13708  hashfacen  14094  hashfacenOLD  14095  hashf1lem1  14096  hashf1lem1OLD  14097  hashf1lem2  14098  0csh0  14434  trclun  14653  dfrtrcl2  14701  shftfval  14709  infcvgaux1i  15497  sursubmefmnd  18450  injsubmefmnd  18451  smndex2dnrinv  18469  symg1bas  18913  pmtrprfvalrn  19011  psgnvali  19031  efgrelexlemb  19271  lss1d  20140  lidldvgen  20439  zndvds  20669  mpfind  21227  pf1ind  21431  cmpsublem  22458  cmpsub  22459  ptpjopn  22671  ptclsg  22674  txdis1cn  22694  tx1stc  22709  hauspwpwf1  23046  qustgplem  23180  ustn0  23280  i1fadd  24764  i1fmul  24765  i1fmulc  24773  ausgrusgri  27441  ushgredgedg  27499  ushgredgedgloop  27501  wspniunwspnon  28189  rusgrnumwwlkb0  28237  fusgr2wsp2nb  28599  nmosetn0  29028  nmoolb  29034  nmlno0lem  29056  nmopsetn0  30128  nmfnsetn0  30141  nmoplb  30170  nmfnlb  30187  nmlnop0iALT  30258  nmopun  30277  nmcexi  30289  branmfn  30368  pjnmopi  30411  fpwrelmapffslem  30969  ldlfcntref  31706  esumc  31919  orvcval2  32325  derangenlem  33033  satfrnmapom  33232  fmlaomn0  33252  fmlasucdisj  33261  dmopab3rexdif  33267  2goelgoanfmla1  33286  mclsssvlem  33424  mclsind  33432  dfon2lem3  33667  dfon2lem7  33671  nosupno  33833  nosupbnd1lem1  33838  noinfno  33848  fnimage  34158  imageval  34159  poimirlem4  35708  poimirlem5  35709  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem9  35713  poimirlem10  35714  poimirlem11  35715  poimirlem12  35716  poimirlem13  35717  poimirlem14  35718  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem18  35722  poimirlem19  35723  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  poimirlem29  35733  poimirlem31  35735  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  itg2addnc  35758  sdclem2  35827  sdclem1  35828  heibor1lem  35894  glbconxN  37319  pmapglbx  37710  dvhb1dimN  38927  sticksstones10  40039  sticksstones11  40040  sticksstones12a  40041  sticksstones12  40042  sticksstones17  40047  sticksstones18  40048  sticksstones19  40049  sn-iotanul  40121  mhphf  40208  eldiophss  40512  setindtrs  40763  hbtlem2  40865  hbtlem5  40869  rngunsnply  40914  dftrcl3  41217  brtrclfv2  41224  dfrtrcl3  41230  dfhe3  41272  elscottab  41751  cpcolld  41765  nzss  41824  upbdrech  42734  fourierdlem36  43574  sge0resplit  43834  hoidmvlelem1  44023  fsetsniunop  44430  elsprel  44815  opeliun2xp  45556  setrec2lem1  46285