Theorem elab 3588

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

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

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 2729

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 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-v 3411

This theorem is referenced by:  ralab  3607  rexab  3609  intab  4868  dfiin2g  4921  dfiunv2  4924  opeliunxp  5588  dmopab2rex  5757  elabrex  6994  abrexco  6995  uniuni  7483  finds  7608  finds2  7610  funcnvuni  7641  fiunlem  7647  fiun  7648  f1iun  7649  mapfset  8439  mapfoss  8441  mapval2  8454  sbthlem2  8650  ssenen  8713  dffi2  8920  dffi3  8928  tctr  9215  tcmin  9216  tc2  9217  tz9.13  9253  tcrank  9346  kardex  9356  karden  9357  cardf2  9405  cardiun  9444  alephval3  9570  dfac3  9581  dfac5lem3  9585  dfac5lem4  9586  dfac2b  9590  kmlem12  9621  cardcf  9712  cfeq0  9716  cfsuc  9717  cff1  9718  cflim2  9723  cfss  9725  axdc3lem2  9911  axdc3lem3  9912  axdclem  9979  brdom7disj  9991  brdom6disj  9992  tskuni  10243  gruina  10278  nqpr  10474  supadd  11645  supmul  11649  dfnn2  11687  dfuzi  12112  seqof  13477  hashfacen  13862  hashfacenOLD  13863  hashf1lem1  13864  hashf1lem1OLD  13865  hashf1lem2  13866  0csh0  14202  trclun  14421  dfrtrcl2  14469  shftfval  14477  infcvgaux1i  15260  sursubmefmnd  18127  injsubmefmnd  18128  smndex2dnrinv  18146  symg1bas  18586  pmtrprfvalrn  18683  psgnvali  18703  efgrelexlemb  18943  lss1d  19803  lidldvgen  20096  zndvds  20317  mpfind  20870  pf1ind  21074  cmpsublem  22099  cmpsub  22100  ptpjopn  22312  ptclsg  22315  txdis1cn  22335  tx1stc  22350  hauspwpwf1  22687  qustgplem  22821  ustn0  22921  i1fadd  24395  i1fmul  24396  i1fmulc  24403  ausgrusgri  27060  ushgredgedg  27118  ushgredgedgloop  27120  wspniunwspnon  27808  rusgrnumwwlkb0  27856  fusgr2wsp2nb  28218  nmosetn0  28647  nmoolb  28653  nmlno0lem  28675  nmopsetn0  29747  nmfnsetn0  29760  nmoplb  29789  nmfnlb  29806  nmlnop0iALT  29877  nmopun  29896  nmcexi  29908  branmfn  29987  pjnmopi  30030  fpwrelmapffslem  30591  ldlfcntref  31325  esumc  31538  orvcval2  31944  derangenlem  32649  satfrnmapom  32848  fmlaomn0  32868  fmlasucdisj  32877  dmopab3rexdif  32883  2goelgoanfmla1  32902  mclsssvlem  33040  mclsind  33048  dfon2lem3  33277  dfon2lem7  33281  nosupno  33471  nosupbnd1lem1  33476  noinfno  33486  fnimage  33780  imageval  33781  poimirlem4  35341  poimirlem5  35342  poimirlem6  35343  poimirlem7  35344  poimirlem8  35345  poimirlem9  35346  poimirlem10  35347  poimirlem11  35348  poimirlem12  35349  poimirlem13  35350  poimirlem14  35351  poimirlem15  35352  poimirlem16  35353  poimirlem17  35354  poimirlem18  35355  poimirlem19  35356  poimirlem20  35357  poimirlem21  35358  poimirlem22  35359  poimirlem25  35362  poimirlem26  35363  poimirlem27  35364  poimirlem29  35366  poimirlem31  35368  mblfinlem3  35376  mblfinlem4  35377  ismblfin  35378  itg2addnc  35391  sdclem2  35460  sdclem1  35461  heibor1lem  35527  glbconxN  36954  pmapglbx  37345  dvhb1dimN  38562  mhphf  39790  eldiophss  40088  setindtrs  40339  hbtlem2  40441  hbtlem5  40445  rngunsnply  40490  dftrcl3  40794  brtrclfv2  40801  dfrtrcl3  40807  dfhe3  40849  elscottab  41325  cpcolld  41339  nzss  41394  upbdrech  42305  fourierdlem36  43151  sge0resplit  43411  hoidmvlelem1  43600  elsprel  44360  opeliun2xp  45101  setrec2lem1  45614