Theorem elab 3615

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 3611	1 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ∈ wcel 2111  {cab 2776  Vcvv 3441

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443

This theorem is referenced by:  ralab  3632  rexab  3634  intab  4868  dfiin2g  4919  dfiunv2  4922  opeliunxp  5583  dmopab2rex  5750  elabrex  6980  abrexco  6981  uniuni  7464  finds  7589  finds2  7591  funcnvuni  7618  fiunlem  7625  fiun  7626  f1iun  7627  mapval2  8419  sbthlem2  8612  ssenen  8675  dffi2  8871  dffi3  8879  tctr  9166  tcmin  9167  tc2  9168  tz9.13  9204  tcrank  9297  kardex  9307  karden  9308  cardf2  9356  cardiun  9395  alephval3  9521  dfac3  9532  dfac5lem3  9536  dfac5lem4  9537  dfac2b  9541  kmlem12  9572  cardcf  9663  cfeq0  9667  cfsuc  9668  cff1  9669  cflim2  9674  cfss  9676  axdc3lem2  9862  axdc3lem3  9863  axdclem  9930  brdom7disj  9942  brdom6disj  9943  tskuni  10194  gruina  10229  nqpr  10425  supadd  11596  supmul  11600  dfnn2  11638  dfuzi  12061  seqof  13423  hashfacen  13808  hashf1lem1  13809  hashf1lem2  13810  0csh0  14146  trclun  14365  dfrtrcl2  14413  shftfval  14421  infcvgaux1i  15204  sursubmefmnd  18053  injsubmefmnd  18054  smndex2dnrinv  18072  symg1bas  18511  pmtrprfvalrn  18608  psgnvali  18628  efgrelexlemb  18868  lss1d  19728  lidldvgen  20021  zndvds  20241  mpfind  20779  pf1ind  20979  cmpsublem  22004  cmpsub  22005  ptpjopn  22217  ptclsg  22220  txdis1cn  22240  tx1stc  22255  hauspwpwf1  22592  qustgplem  22726  ustn0  22826  i1fadd  24299  i1fmul  24300  i1fmulc  24307  ausgrusgri  26961  ushgredgedg  27019  ushgredgedgloop  27021  wspniunwspnon  27709  rusgrnumwwlkb0  27757  fusgr2wsp2nb  28119  nmosetn0  28548  nmoolb  28554  nmlno0lem  28576  nmopsetn0  29648  nmfnsetn0  29661  nmoplb  29690  nmfnlb  29707  nmlnop0iALT  29778  nmopun  29797  nmcexi  29809  branmfn  29888  pjnmopi  29931  fpwrelmapffslem  30494  ldlfcntref  31207  esumc  31420  orvcval2  31826  derangenlem  32531  satfrnmapom  32730  fmlaomn0  32750  fmlasucdisj  32759  dmopab3rexdif  32765  2goelgoanfmla1  32784  mclsssvlem  32922  mclsind  32930  dfon2lem3  33143  dfon2lem7  33147  nosupno  33316  nosupbnd1lem1  33321  fnimage  33503  imageval  33504  poimirlem4  35061  poimirlem5  35062  poimirlem6  35063  poimirlem7  35064  poimirlem8  35065  poimirlem9  35066  poimirlem10  35067  poimirlem11  35068  poimirlem12  35069  poimirlem13  35070  poimirlem14  35071  poimirlem15  35072  poimirlem16  35073  poimirlem17  35074  poimirlem18  35075  poimirlem19  35076  poimirlem20  35077  poimirlem21  35078  poimirlem22  35079  poimirlem25  35082  poimirlem26  35083  poimirlem27  35084  poimirlem29  35086  poimirlem31  35088  mblfinlem3  35096  mblfinlem4  35097  ismblfin  35098  itg2addnc  35111  sdclem2  35180  sdclem1  35181  heibor1lem  35247  glbconxN  36674  pmapglbx  37065  dvhb1dimN  38282  eldiophss  39715  setindtrs  39966  hbtlem2  40068  hbtlem5  40072  rngunsnply  40117  dftrcl3  40421  brtrclfv2  40428  dfrtrcl3  40434  dfhe3  40476  elscottab  40952  cpcolld  40966  nzss  41021  upbdrech  41937  fourierdlem36  42785  sge0resplit  43045  hoidmvlelem1  43234  elsprel  43992  opeliun2xp  44734  setrec2lem1  45223