Theorem elab 3619

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810

This theorem is referenced by:  intab  4910  dfiun2g  4961  dfiin2g  4962  dfiunv2  4965  opeliunxp  5687  opeliun2xp  5688  dmopab2rex  5861  iotanul2  6460  elabrex  7186  abrexco  7188  uniuni  7705  finds  7836  finds2  7838  funcnvuni  7872  fiunlem  7884  fiun  7885  f1iun  7886  mapfset  8786  mapfoss  8788  fsetsspwxp  8789  mapval2  8809  sbthlem2  9015  ssenen  9078  dffi2  9325  dffi3  9333  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  12113  supmul  12117  dfnn2  12176  dfuzi  12609  seqof  14010  hashfacen  14405  hashf1lem1  14406  hashf1lem2  14407  0csh0  14744  trclun  14965  dfrtrcl2  15013  shftfval  15021  infcvgaux1i  15811  sursubmefmnd  18853  injsubmefmnd  18854  smndex2dnrinv  18875  symg1bas  19355  pmtrprfvalrn  19452  psgnvali  19472  efgrelexlemb  19714  lss1d  20947  lidldvgen  21321  zndvds  21518  mpfind  22082  pf1ind  22308  cmpsublem  23352  cmpsub  23353  ptpjopn  23565  ptclsg  23568  txdis1cn  23588  tx1stc  23603  hauspwpwf1  23940  qustgplem  24074  ustn0  24174  i1fadd  25650  i1fmul  25651  i1fmulc  25658  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  29979  rusgrnumwwlkb0  30030  fusgr2wsp2nb  30392  nmosetn0  30824  nmoolb  30830  nmlno0lem  30852  nmopsetn0  31924  nmfnsetn0  31937  nmoplb  31966  nmfnlb  31983  nmlnop0iALT  32054  nmopun  32073  nmcexi  32085  branmfn  32164  pjnmopi  32207  fpwrelmapffslem  32793  ldlfcntref  33986  esumc  34183  orvcval2  34591  derangenlem  35341  satfrnmapom  35540  fmlaomn0  35560  fmlasucdisj  35569  dmopab3rexdif  35575  2goelgoanfmla1  35594  mclsssvlem  35732  mclsind  35740  dfon2lem3  35953  dfon2lem7  35957  fnimage  36097  imageval  36098  dfttc4  36700  poimirlem4  37933  poimirlem5  37934  poimirlem6  37935  poimirlem7  37936  poimirlem8  37937  poimirlem9  37938  poimirlem10  37939  poimirlem11  37940  poimirlem12  37941  poimirlem13  37942  poimirlem14  37943  poimirlem15  37944  poimirlem16  37945  poimirlem17  37946  poimirlem18  37947  poimirlem19  37948  poimirlem20  37949  poimirlem21  37950  poimirlem22  37951  poimirlem25  37954  poimirlem26  37955  poimirlem27  37956  poimirlem29  37958  poimirlem31  37960  mblfinlem3  37968  mblfinlem4  37969  ismblfin  37970  itg2addnc  37983  sdclem2  38051  sdclem1  38052  heibor1lem  38118  glbconxN  39812  pmapglbx  40203  dvhb1dimN  41420  sticksstones10  42582  sticksstones11  42583  sticksstones12a  42584  sticksstones12  42585  sticksstones17  42590  sticksstones18  42591  sticksstones19  42592  redvmptabs  42780  abbibw  43098  eldiophss  43194  setindtrs  43441  hbtlem2  43540  hbtlem5  43544  rngunsnply  43585  oaun3lem1  43790  oadif1lem  43795  oadif1  43796  dftrcl3  44135  brtrclfv2  44142  dfrtrcl3  44148  dfhe3  44190  elscottab  44659  cpcolld  44673  nzss  44732  upbdrech  45726  fourierdlem36  46559  sge0resplit  46822  hoidmvlelem1  47011  fsetsniunop  47485  elsprel  47923  ixpv  49353  iinfconstbas  49529  setrec2lem1  50156