Theorem elab 3635

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

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

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  4934  dfiun2g  4986  dfiin2g  4987  dfiunv2  4990  opeliunxp  5692  opeliun2xp  5693  dmopab2rex  5867  iotanul2  6466  elabrex  7190  abrexco  7192  uniuni  7709  finds  7840  finds2  7842  funcnvuni  7876  fiunlem  7888  fiun  7889  f1iun  7890  mapfset  8791  mapfoss  8793  fsetsspwxp  8794  mapval2  8814  sbthlem2  9020  ssenen  9083  dffi2  9330  dffi3  9338  tctr  9651  tcmin  9652  tc2  9653  tz9.13  9707  tcrank  9800  kardex  9810  karden  9811  cardf2  9859  cardiun  9898  alephval3  10024  dfac3  10035  dfac5lem3  10039  dfac5lem4  10040  dfac5lem4OLD  10042  dfac2b  10045  kmlem12  10076  cardcf  10166  cfeq0  10170  cfsuc  10171  cff1  10172  cflim2  10177  cfss  10179  axdc3lem2  10365  axdc3lem3  10366  axdclem  10433  brdom7disj  10445  brdom6disj  10446  tskuni  10698  gruina  10733  nqpr  10929  supadd  12114  supmul  12118  dfnn2  12162  dfuzi  12587  seqof  13986  hashfacen  14381  hashf1lem1  14382  hashf1lem2  14383  0csh0  14720  trclun  14941  dfrtrcl2  14989  shftfval  14997  infcvgaux1i  15784  sursubmefmnd  18825  injsubmefmnd  18826  smndex2dnrinv  18844  symg1bas  19324  pmtrprfvalrn  19421  psgnvali  19441  efgrelexlemb  19683  lss1d  20918  lidldvgen  21293  zndvds  21508  mpfind  22074  pf1ind  22303  cmpsublem  23347  cmpsub  23348  ptpjopn  23560  ptclsg  23563  txdis1cn  23583  tx1stc  23598  hauspwpwf1  23935  qustgplem  24069  ustn0  24169  i1fadd  25656  i1fmul  25657  i1fmulc  25664  nosupno  27675  nosupbnd1lem1  27680  noinfno  27690  addsproplem2  27952  addsproplem4  27954  addsproplem5  27955  addsproplem6  27956  addsuniflem  27983  negsid  28023  mulsproplem9  28106  mulsproplem12  28109  ssltmul1  28129  ssltmul2  28130  precsexlem9  28196  precsexlem11  28198  dfn0s2  28312  recut  28473  elreno2  28474  ausgrusgri  29224  ushgredgedg  29285  ushgredgedgloop  29287  wspniunwspnon  29979  rusgrnumwwlkb0  30030  fusgr2wsp2nb  30392  nmosetn0  30823  nmoolb  30829  nmlno0lem  30851  nmopsetn0  31923  nmfnsetn0  31936  nmoplb  31965  nmfnlb  31982  nmlnop0iALT  32053  nmopun  32072  nmcexi  32084  branmfn  32163  pjnmopi  32206  fpwrelmapffslem  32792  ldlfcntref  33992  esumc  34189  orvcval2  34597  derangenlem  35346  satfrnmapom  35545  fmlaomn0  35565  fmlasucdisj  35574  dmopab3rexdif  35580  2goelgoanfmla1  35599  mclsssvlem  35737  mclsind  35745  dfon2lem3  35958  dfon2lem7  35962  fnimage  36102  imageval  36103  poimirlem4  37796  poimirlem5  37797  poimirlem6  37798  poimirlem7  37799  poimirlem8  37800  poimirlem9  37801  poimirlem10  37802  poimirlem11  37803  poimirlem12  37804  poimirlem13  37805  poimirlem14  37806  poimirlem15  37807  poimirlem16  37808  poimirlem17  37809  poimirlem18  37810  poimirlem19  37811  poimirlem20  37812  poimirlem21  37813  poimirlem22  37814  poimirlem25  37817  poimirlem26  37818  poimirlem27  37819  poimirlem29  37821  poimirlem31  37823  mblfinlem3  37831  mblfinlem4  37832  ismblfin  37833  itg2addnc  37846  sdclem2  37914  sdclem1  37915  heibor1lem  37981  glbconxN  39675  pmapglbx  40066  dvhb1dimN  41283  sticksstones10  42446  sticksstones11  42447  sticksstones12a  42448  sticksstones12  42449  sticksstones17  42454  sticksstones18  42455  sticksstones19  42456  redvmptabs  42651  abbibw  42956  eldiophss  43052  setindtrs  43303  hbtlem2  43402  hbtlem5  43406  rngunsnply  43447  oaun3lem1  43652  oadif1lem  43657  oadif1  43658  dftrcl3  43997  brtrclfv2  44004  dfrtrcl3  44010  dfhe3  44052  elscottab  44521  cpcolld  44535  nzss  44594  upbdrech  45589  fourierdlem36  46423  sge0resplit  46686  hoidmvlelem1  46875  fsetsniunop  47331  elsprel  47757  ixpv  49171  iinfconstbas  49347  setrec2lem1  49974