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  5698  opeliun2xp  5699  dmopab2rex  5873  iotanul2  6472  elabrex  7197  abrexco  7199  uniuni  7716  finds  7847  finds2  7849  funcnvuni  7883  fiunlem  7895  fiun  7896  f1iun  7897  mapfset  8797  mapfoss  8799  fsetsspwxp  8800  mapval2  8820  sbthlem2  9026  ssenen  9089  dffi2  9336  dffi3  9344  tctr  9659  tcmin  9660  tc2  9661  tz9.13  9715  tcrank  9808  kardex  9818  karden  9819  cardf2  9867  cardiun  9906  alephval3  10032  dfac3  10043  dfac5lem3  10047  dfac5lem4  10048  dfac5lem4OLD  10050  dfac2b  10053  kmlem12  10084  cardcf  10174  cfeq0  10178  cfsuc  10179  cff1  10180  cflim2  10185  cfss  10187  axdc3lem2  10373  axdc3lem3  10374  axdclem  10441  brdom7disj  10453  brdom6disj  10454  tskuni  10706  gruina  10741  nqpr  10937  supadd  12124  supmul  12128  dfnn2  12187  dfuzi  12620  seqof  14021  hashfacen  14416  hashf1lem1  14417  hashf1lem2  14418  0csh0  14755  trclun  14976  dfrtrcl2  15024  shftfval  15032  infcvgaux1i  15822  sursubmefmnd  18864  injsubmefmnd  18865  smndex2dnrinv  18886  symg1bas  19366  pmtrprfvalrn  19463  psgnvali  19483  efgrelexlemb  19725  lss1d  20958  lidldvgen  21332  zndvds  21529  mpfind  22093  pf1ind  22320  cmpsublem  23364  cmpsub  23365  ptpjopn  23577  ptclsg  23580  txdis1cn  23600  tx1stc  23615  hauspwpwf1  23952  qustgplem  24086  ustn0  24186  i1fadd  25662  i1fmul  25663  i1fmulc  25670  nosupno  27667  nosupbnd1lem1  27672  noinfno  27682  addsproplem2  27962  addsproplem4  27964  addsproplem5  27965  addsproplem6  27966  addsuniflem  27993  negsid  28033  mulsproplem9  28116  mulsproplem12  28119  sltmuls1  28139  sltmuls2  28140  precsexlem9  28207  precsexlem11  28209  dfn0s2  28324  recut  28486  elreno2  28487  ausgrusgri  29237  ushgredgedg  29298  ushgredgedgloop  29300  wspniunwspnon  29991  rusgrnumwwlkb0  30042  fusgr2wsp2nb  30404  nmosetn0  30836  nmoolb  30842  nmlno0lem  30864  nmopsetn0  31936  nmfnsetn0  31949  nmoplb  31978  nmfnlb  31995  nmlnop0iALT  32066  nmopun  32085  nmcexi  32097  branmfn  32176  pjnmopi  32219  fpwrelmapffslem  32805  ldlfcntref  33998  esumc  34195  orvcval2  34603  derangenlem  35353  satfrnmapom  35552  fmlaomn0  35572  fmlasucdisj  35581  dmopab3rexdif  35587  2goelgoanfmla1  35606  mclsssvlem  35744  mclsind  35752  dfon2lem3  35965  dfon2lem7  35969  fnimage  36109  imageval  36110  dfttc4  36712  poimirlem4  37945  poimirlem5  37946  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem9  37950  poimirlem10  37951  poimirlem11  37952  poimirlem12  37953  poimirlem13  37954  poimirlem14  37955  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem18  37959  poimirlem19  37960  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  poimirlem29  37970  poimirlem31  37972  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  itg2addnc  37995  sdclem2  38063  sdclem1  38064  heibor1lem  38130  glbconxN  39824  pmapglbx  40215  dvhb1dimN  41432  sticksstones10  42594  sticksstones11  42595  sticksstones12a  42596  sticksstones12  42597  sticksstones17  42602  sticksstones18  42603  sticksstones19  42604  redvmptabs  42792  abbibw  43110  eldiophss  43206  setindtrs  43453  hbtlem2  43552  hbtlem5  43556  rngunsnply  43597  oaun3lem1  43802  oadif1lem  43807  oadif1  43808  dftrcl3  44147  brtrclfv2  44154  dfrtrcl3  44160  dfhe3  44202  elscottab  44671  cpcolld  44685  nzss  44744  upbdrech  45738  fourierdlem36  46571  sge0resplit  46834  hoidmvlelem1  47023  fsetsniunop  47491  elsprel  47929  ixpv  49359  iinfconstbas  49535  setrec2lem1  50162