Theorem elab 3623

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

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

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  4921  dfiun2g  4973  dfiin2g  4974  dfiunv2  4977  opeliunxp  5689  opeliun2xp  5690  dmopab2rex  5864  iotanul2  6463  elabrex  7188  abrexco  7190  uniuni  7707  finds  7838  finds2  7840  funcnvuni  7874  fiunlem  7886  fiun  7887  f1iun  7888  mapfset  8788  mapfoss  8790  fsetsspwxp  8791  mapval2  8811  sbthlem2  9017  ssenen  9080  dffi2  9327  dffi3  9335  tctr  9648  tcmin  9649  tc2  9650  tz9.13  9704  tcrank  9797  kardex  9807  karden  9808  cardf2  9856  cardiun  9895  alephval3  10021  dfac3  10032  dfac5lem3  10036  dfac5lem4  10037  dfac5lem4OLD  10039  dfac2b  10042  kmlem12  10073  cardcf  10163  cfeq0  10167  cfsuc  10168  cff1  10169  cflim2  10174  cfss  10176  axdc3lem2  10362  axdc3lem3  10363  axdclem  10430  brdom7disj  10442  brdom6disj  10443  tskuni  10695  gruina  10730  nqpr  10926  supadd  12111  supmul  12115  dfnn2  12159  dfuzi  12584  seqof  13983  hashfacen  14378  hashf1lem1  14379  hashf1lem2  14380  0csh0  14717  trclun  14938  dfrtrcl2  14986  shftfval  14994  infcvgaux1i  15781  sursubmefmnd  18822  injsubmefmnd  18823  smndex2dnrinv  18844  symg1bas  19324  pmtrprfvalrn  19421  psgnvali  19441  efgrelexlemb  19683  lss1d  20916  lidldvgen  21291  zndvds  21506  mpfind  22071  pf1ind  22298  cmpsublem  23342  cmpsub  23343  ptpjopn  23555  ptclsg  23558  txdis1cn  23578  tx1stc  23593  hauspwpwf1  23930  qustgplem  24064  ustn0  24164  i1fadd  25640  i1fmul  25641  i1fmulc  25648  nosupno  27655  nosupbnd1lem1  27660  noinfno  27670  addsproplem2  27950  addsproplem4  27952  addsproplem5  27953  addsproplem6  27954  addsuniflem  27981  negsid  28021  mulsproplem9  28104  mulsproplem12  28107  sltmuls1  28127  sltmuls2  28128  precsexlem9  28195  precsexlem11  28197  dfn0s2  28312  recut  28474  elreno2  28475  ausgrusgri  29225  ushgredgedg  29286  ushgredgedgloop  29288  wspniunwspnon  29980  rusgrnumwwlkb0  30031  fusgr2wsp2nb  30393  nmosetn0  30825  nmoolb  30831  nmlno0lem  30853  nmopsetn0  31925  nmfnsetn0  31938  nmoplb  31967  nmfnlb  31984  nmlnop0iALT  32055  nmopun  32074  nmcexi  32086  branmfn  32165  pjnmopi  32208  fpwrelmapffslem  32794  ldlfcntref  34004  esumc  34201  orvcval2  34609  derangenlem  35359  satfrnmapom  35558  fmlaomn0  35578  fmlasucdisj  35587  dmopab3rexdif  35593  2goelgoanfmla1  35612  mclsssvlem  35750  mclsind  35758  dfon2lem3  35971  dfon2lem7  35975  fnimage  36115  imageval  36116  dfttc4  36718  poimirlem4  37936  poimirlem5  37937  poimirlem6  37938  poimirlem7  37939  poimirlem8  37940  poimirlem9  37941  poimirlem10  37942  poimirlem11  37943  poimirlem12  37944  poimirlem13  37945  poimirlem14  37946  poimirlem15  37947  poimirlem16  37948  poimirlem17  37949  poimirlem18  37950  poimirlem19  37951  poimirlem20  37952  poimirlem21  37953  poimirlem22  37954  poimirlem25  37957  poimirlem26  37958  poimirlem27  37959  poimirlem29  37961  poimirlem31  37963  mblfinlem3  37971  mblfinlem4  37972  ismblfin  37973  itg2addnc  37986  sdclem2  38054  sdclem1  38055  heibor1lem  38121  glbconxN  39815  pmapglbx  40206  dvhb1dimN  41423  sticksstones10  42586  sticksstones11  42587  sticksstones12a  42588  sticksstones12  42589  sticksstones17  42594  sticksstones18  42595  sticksstones19  42596  redvmptabs  42791  abbibw  43109  eldiophss  43205  setindtrs  43456  hbtlem2  43555  hbtlem5  43559  rngunsnply  43600  oaun3lem1  43805  oadif1lem  43810  oadif1  43811  dftrcl3  44150  brtrclfv2  44157  dfrtrcl3  44163  dfhe3  44205  elscottab  44674  cpcolld  44688  nzss  44747  upbdrech  45741  fourierdlem36  46575  sge0resplit  46838  hoidmvlelem1  47027  fsetsniunop  47483  elsprel  47909  ixpv  49323  iinfconstbas  49499  setrec2lem1  50126