Theorem elab 3653

Description: Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. (Contributed by NM, 1-Aug-1994.)

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		nfv 1915	. 2 ⊢ Ⅎ𝑥𝜓
2		elab.1	. 2 ⊢ 𝐴 ∈ V
3		elab.2	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	1, 2, 3	elabf 3651	1 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537   ∈ wcel 2114  {cab 2798  Vcvv 3481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-v 3483

This theorem is referenced by:  ralab  3670  rexab  3672  intab  4887  dfiin2g  4938  dfiunv2  4941  opeliunxp  5600  dmopab2rex  5767  elabrex  6983  abrexco  6984  uniuni  7465  finds  7589  finds2  7591  funcnvuni  7617  fiunlem  7624  fiun  7625  f1iun  7626  mapval2  8417  sbthlem2  8609  ssenen  8672  dffi2  8868  dffi3  8876  tctr  9163  tcmin  9164  tc2  9165  tz9.13  9201  tcrank  9294  kardex  9304  karden  9305  cardf2  9353  cardiun  9392  alephval3  9517  dfac3  9528  dfac5lem3  9532  dfac5lem4  9533  dfac2b  9537  kmlem12  9568  cardcf  9655  cfeq0  9659  cfsuc  9660  cff1  9661  cflim2  9666  cfss  9668  axdc3lem2  9854  axdc3lem3  9855  axdclem  9922  brdom7disj  9934  brdom6disj  9935  tskuni  10186  gruina  10221  nqpr  10417  supadd  11590  supmul  11594  dfnn2  11632  dfuzi  12055  seqof  13412  hashfacen  13797  hashf1lem1  13798  hashf1lem2  13799  0csh0  14135  trclun  14354  dfrtrcl2  14401  shftfval  14409  infcvgaux1i  15192  sursubmefmnd  18039  injsubmefmnd  18040  smndex2dnrinv  18058  symg1bas  18497  pmtrprfvalrn  18594  psgnvali  18614  efgrelexlemb  18854  lss1d  19713  lidldvgen  20006  mpfind  20298  pf1ind  20496  zndvds  20674  cmpsublem  21985  cmpsub  21986  ptpjopn  22198  ptclsg  22201  txdis1cn  22221  tx1stc  22236  hauspwpwf1  22573  qustgplem  22707  ustn0  22807  i1fadd  24274  i1fmul  24275  i1fmulc  24282  ausgrusgri  26934  ushgredgedg  26992  ushgredgedgloop  26994  wspniunwspnon  27682  rusgrnumwwlkb0  27730  fusgr2wsp2nb  28092  nmosetn0  28521  nmoolb  28527  nmlno0lem  28549  nmopsetn0  29621  nmfnsetn0  29634  nmoplb  29663  nmfnlb  29680  nmlnop0iALT  29751  nmopun  29770  nmcexi  29782  branmfn  29861  pjnmopi  29904  fpwrelmapffslem  30449  ldlfcntref  31123  esumc  31312  orvcval2  31718  derangenlem  32420  satfrnmapom  32619  fmlaomn0  32639  fmlasucdisj  32648  dmopab3rexdif  32654  2goelgoanfmla1  32673  mclsssvlem  32811  mclsind  32819  dfon2lem3  33032  dfon2lem7  33036  nosupno  33205  nosupbnd1lem1  33210  fnimage  33392  imageval  33393  poimirlem4  34925  poimirlem5  34926  poimirlem6  34927  poimirlem7  34928  poimirlem8  34929  poimirlem9  34930  poimirlem10  34931  poimirlem11  34932  poimirlem12  34933  poimirlem13  34934  poimirlem14  34935  poimirlem15  34936  poimirlem16  34937  poimirlem17  34938  poimirlem18  34939  poimirlem19  34940  poimirlem20  34941  poimirlem21  34942  poimirlem22  34943  poimirlem25  34946  poimirlem26  34947  poimirlem27  34948  poimirlem29  34950  poimirlem31  34952  mblfinlem3  34960  mblfinlem4  34961  ismblfin  34962  itg2addnc  34975  sdclem2  35044  sdclem1  35045  heibor1lem  35114  glbconxN  36541  pmapglbx  36932  dvhb1dimN  38149  eldiophss  39458  setindtrs  39709  hbtlem2  39811  hbtlem5  39815  rngunsnply  39860  dftrcl3  40150  brtrclfv2  40157  dfrtrcl3  40163  dfhe3  40206  elscottab  40665  cpcolld  40679  nzss  40734  upbdrech  41657  fourierdlem36  42513  sge0resplit  42773  hoidmvlelem1  42962  elsprel  43717  opeliun2xp  44461  setrec2lem1  44876