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 2142, ax-11 2158, ax-12 2178. (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 1540   ∈ wcel 2109  {cab 2714  Vcvv 3464

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810

This theorem is referenced by:  intab  4959  dfiun2g  5011  dfiin2g  5013  dfiunv2  5016  opeliunxp  5726  opeliun2xp  5727  dmopab2rex  5902  iotanul2  6506  elabrex  7239  abrexco  7241  uniuni  7761  finds  7897  finds2  7899  funcnvuni  7933  fiunlem  7945  fiun  7946  f1iun  7947  mapfset  8869  mapfoss  8871  fsetsspwxp  8872  mapval2  8891  sbthlem2  9103  ssenen  9170  dffi2  9440  dffi3  9448  tctr  9759  tcmin  9760  tc2  9761  tz9.13  9810  tcrank  9903  kardex  9913  karden  9914  cardf2  9962  cardiun  10001  alephval3  10129  dfac3  10140  dfac5lem3  10144  dfac5lem4  10145  dfac5lem4OLD  10147  dfac2b  10150  kmlem12  10181  cardcf  10271  cfeq0  10275  cfsuc  10276  cff1  10277  cflim2  10282  cfss  10284  axdc3lem2  10470  axdc3lem3  10471  axdclem  10538  brdom7disj  10550  brdom6disj  10551  tskuni  10802  gruina  10837  nqpr  11033  supadd  12215  supmul  12219  dfnn2  12258  dfuzi  12689  seqof  14082  hashfacen  14477  hashf1lem1  14478  hashf1lem2  14479  0csh0  14816  trclun  15038  dfrtrcl2  15086  shftfval  15094  infcvgaux1i  15878  sursubmefmnd  18879  injsubmefmnd  18880  smndex2dnrinv  18898  symg1bas  19377  pmtrprfvalrn  19474  psgnvali  19494  efgrelexlemb  19736  lss1d  20925  lidldvgen  21300  zndvds  21515  mpfind  22070  pf1ind  22298  cmpsublem  23342  cmpsub  23343  ptpjopn  23555  ptclsg  23558  txdis1cn  23578  tx1stc  23593  hauspwpwf1  23930  qustgplem  24064  ustn0  24164  i1fadd  25653  i1fmul  25654  i1fmulc  25661  nosupno  27672  nosupbnd1lem1  27677  noinfno  27687  addsproplem2  27934  addsproplem4  27936  addsproplem5  27937  addsproplem6  27938  addsuniflem  27965  negsid  28004  mulsproplem9  28084  mulsproplem12  28087  ssltmul1  28107  ssltmul2  28108  precsexlem9  28174  precsexlem11  28176  dfn0s2  28281  recut  28404  0reno  28405  ausgrusgri  29152  ushgredgedg  29213  ushgredgedgloop  29215  wspniunwspnon  29910  rusgrnumwwlkb0  29958  fusgr2wsp2nb  30320  nmosetn0  30751  nmoolb  30757  nmlno0lem  30779  nmopsetn0  31851  nmfnsetn0  31864  nmoplb  31893  nmfnlb  31910  nmlnop0iALT  31981  nmopun  32000  nmcexi  32012  branmfn  32091  pjnmopi  32134  fpwrelmapffslem  32714  ldlfcntref  33890  esumc  34087  orvcval2  34496  derangenlem  35198  satfrnmapom  35397  fmlaomn0  35417  fmlasucdisj  35426  dmopab3rexdif  35432  2goelgoanfmla1  35451  mclsssvlem  35589  mclsind  35597  dfon2lem3  35808  dfon2lem7  35812  fnimage  35952  imageval  35953  poimirlem4  37653  poimirlem5  37654  poimirlem6  37655  poimirlem7  37656  poimirlem8  37657  poimirlem9  37658  poimirlem10  37659  poimirlem11  37660  poimirlem12  37661  poimirlem13  37662  poimirlem14  37663  poimirlem15  37664  poimirlem16  37665  poimirlem17  37666  poimirlem18  37667  poimirlem19  37668  poimirlem20  37669  poimirlem21  37670  poimirlem22  37671  poimirlem25  37674  poimirlem26  37675  poimirlem27  37676  poimirlem29  37678  poimirlem31  37680  mblfinlem3  37688  mblfinlem4  37689  ismblfin  37690  itg2addnc  37703  sdclem2  37771  sdclem1  37772  heibor1lem  37838  glbconxN  39402  pmapglbx  39793  dvhb1dimN  41010  sticksstones10  42173  sticksstones11  42174  sticksstones12a  42175  sticksstones12  42176  sticksstones17  42181  sticksstones18  42182  sticksstones19  42183  redvmptabs  42378  abbibw  42675  eldiophss  42772  setindtrs  43024  hbtlem2  43123  hbtlem5  43127  rngunsnply  43168  oaun3lem1  43373  oadif1lem  43378  oadif1  43379  dftrcl3  43719  brtrclfv2  43726  dfrtrcl3  43732  dfhe3  43774  elscottab  44243  cpcolld  44257  nzss  44316  upbdrech  45314  fourierdlem36  46152  sge0resplit  46415  hoidmvlelem1  46604  fsetsniunop  47058  elsprel  47469  ixpv  48845  iinfconstbas  49013  setrec2lem1  49537