Theorem elab 3663

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1539   ∈ wcel 2107  {cab 2712  Vcvv 3464

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808

This theorem is referenced by:  ralabOLD  3682  rexabOLD  3685  intab  4960  dfiun2g  5012  dfiin2g  5014  dfiunv2  5017  opeliunxp  5734  opeliun2xp  5735  dmopab2rex  5910  iotanul2  6512  elabrex  7245  abrexco  7247  uniuni  7765  finds  7901  finds2  7903  funcnvuni  7937  fiunlem  7949  fiun  7950  f1iun  7951  mapfset  8873  mapfoss  8875  fsetsspwxp  8876  mapval2  8895  sbthlem2  9107  ssenen  9174  dffi2  9446  dffi3  9454  tctr  9763  tcmin  9764  tc2  9765  tz9.13  9814  tcrank  9907  kardex  9917  karden  9918  cardf2  9966  cardiun  10005  alephval3  10133  dfac3  10144  dfac5lem3  10148  dfac5lem4  10149  dfac5lem4OLD  10151  dfac2b  10154  kmlem12  10185  cardcf  10275  cfeq0  10279  cfsuc  10280  cff1  10281  cflim2  10286  cfss  10288  axdc3lem2  10474  axdc3lem3  10475  axdclem  10542  brdom7disj  10554  brdom6disj  10555  tskuni  10806  gruina  10841  nqpr  11037  supadd  12219  supmul  12223  dfnn2  12262  dfuzi  12693  seqof  14083  hashfacen  14476  hashf1lem1  14477  hashf1lem2  14478  0csh0  14814  trclun  15036  dfrtrcl2  15084  shftfval  15092  infcvgaux1i  15876  sursubmefmnd  18883  injsubmefmnd  18884  smndex2dnrinv  18902  symg1bas  19381  pmtrprfvalrn  19479  psgnvali  19499  efgrelexlemb  19741  lss1d  20934  lidldvgen  21311  zndvds  21535  mpfind  22098  pf1ind  22326  cmpsublem  23372  cmpsub  23373  ptpjopn  23585  ptclsg  23588  txdis1cn  23608  tx1stc  23623  hauspwpwf1  23960  qustgplem  24094  ustn0  24194  i1fadd  25685  i1fmul  25686  i1fmulc  25693  nosupno  27703  nosupbnd1lem1  27708  noinfno  27718  addsproplem2  27958  addsproplem4  27960  addsproplem5  27961  addsproplem6  27962  addsuniflem  27989  negsid  28028  mulsproplem9  28105  mulsproplem12  28108  ssltmul1  28128  ssltmul2  28129  precsexlem9  28194  precsexlem11  28196  dfn0s2  28291  recut  28383  0reno  28384  ausgrusgri  29132  ushgredgedg  29193  ushgredgedgloop  29195  wspniunwspnon  29890  rusgrnumwwlkb0  29938  fusgr2wsp2nb  30300  nmosetn0  30731  nmoolb  30737  nmlno0lem  30759  nmopsetn0  31831  nmfnsetn0  31844  nmoplb  31873  nmfnlb  31890  nmlnop0iALT  31961  nmopun  31980  nmcexi  31992  branmfn  32071  pjnmopi  32114  fpwrelmapffslem  32690  ldlfcntref  33794  esumc  33993  orvcval2  34402  derangenlem  35117  satfrnmapom  35316  fmlaomn0  35336  fmlasucdisj  35345  dmopab3rexdif  35351  2goelgoanfmla1  35370  mclsssvlem  35508  mclsind  35516  dfon2lem3  35727  dfon2lem7  35731  fnimage  35871  imageval  35872  poimirlem4  37572  poimirlem5  37573  poimirlem6  37574  poimirlem7  37575  poimirlem8  37576  poimirlem9  37577  poimirlem10  37578  poimirlem11  37579  poimirlem12  37580  poimirlem13  37581  poimirlem14  37582  poimirlem15  37583  poimirlem16  37584  poimirlem17  37585  poimirlem18  37586  poimirlem19  37587  poimirlem20  37588  poimirlem21  37589  poimirlem22  37590  poimirlem25  37593  poimirlem26  37594  poimirlem27  37595  poimirlem29  37597  poimirlem31  37599  mblfinlem3  37607  mblfinlem4  37608  ismblfin  37609  itg2addnc  37622  sdclem2  37690  sdclem1  37691  heibor1lem  37757  glbconxN  39321  pmapglbx  39712  dvhb1dimN  40929  sticksstones10  42097  sticksstones11  42098  sticksstones12a  42099  sticksstones12  42100  sticksstones17  42105  sticksstones18  42106  sticksstones19  42107  redvmptabs  42335  abbibw  42632  eldiophss  42730  setindtrs  42982  hbtlem2  43081  hbtlem5  43085  rngunsnply  43126  oaun3lem1  43332  oadif1lem  43337  oadif1  43338  dftrcl3  43678  brtrclfv2  43685  dfrtrcl3  43691  dfhe3  43733  elscottab  44208  cpcolld  44222  nzss  44281  upbdrech  45262  fourierdlem36  46103  sge0resplit  46366  hoidmvlelem1  46555  fsetsniunop  47007  elsprel  47408  setrec2lem1  49208