Theorem elab 3666

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1533   ∈ wcel 2110  {cab 2799  Vcvv 3494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496

This theorem is referenced by:  ralab  3683  rexab  3685  intab  4898  dfiin2g  4949  dfiunv2  4952  opeliunxp  5613  dmopab2rex  5780  elabrex  6996  abrexco  6997  uniuni  7478  finds  7602  finds2  7604  funcnvuni  7630  fiunlem  7637  fiun  7638  f1iun  7639  mapval2  8430  sbthlem2  8622  ssenen  8685  dffi2  8881  dffi3  8889  tctr  9176  tcmin  9177  tc2  9178  tz9.13  9214  tcrank  9307  kardex  9317  karden  9318  cardf2  9366  cardiun  9405  alephval3  9530  dfac3  9541  dfac5lem3  9545  dfac5lem4  9546  dfac2b  9550  kmlem12  9581  cardcf  9668  cfeq0  9672  cfsuc  9673  cff1  9674  cflim2  9679  cfss  9681  axdc3lem2  9867  axdc3lem3  9868  axdclem  9935  brdom7disj  9947  brdom6disj  9948  tskuni  10199  gruina  10234  nqpr  10430  supadd  11603  supmul  11607  dfnn2  11645  dfuzi  12067  seqof  13421  hashfacen  13806  hashf1lem1  13807  hashf1lem2  13808  0csh0  14149  trclun  14368  dfrtrcl2  14415  shftfval  14423  infcvgaux1i  15206  sursubmefmnd  18055  injsubmefmnd  18056  smndex2dnrinv  18074  symg1bas  18513  pmtrprfvalrn  18610  psgnvali  18630  efgrelexlemb  18870  lss1d  19729  lidldvgen  20022  mpfind  20314  pf1ind  20512  zndvds  20690  cmpsublem  22001  cmpsub  22002  ptpjopn  22214  ptclsg  22217  txdis1cn  22237  tx1stc  22252  hauspwpwf1  22589  qustgplem  22723  ustn0  22823  i1fadd  24290  i1fmul  24291  i1fmulc  24298  ausgrusgri  26947  ushgredgedg  27005  ushgredgedgloop  27007  wspniunwspnon  27696  rusgrnumwwlkb0  27744  fusgr2wsp2nb  28107  nmosetn0  28536  nmoolb  28542  nmlno0lem  28564  nmopsetn0  29636  nmfnsetn0  29649  nmoplb  29678  nmfnlb  29695  nmlnop0iALT  29766  nmopun  29785  nmcexi  29797  branmfn  29876  pjnmopi  29919  fpwrelmapffslem  30462  ldlfcntref  31113  esumc  31305  orvcval2  31711  derangenlem  32413  satfrnmapom  32612  fmlaomn0  32632  fmlasucdisj  32641  dmopab3rexdif  32647  2goelgoanfmla1  32666  mclsssvlem  32804  mclsind  32812  dfon2lem3  33025  dfon2lem7  33029  nosupno  33198  nosupbnd1lem1  33203  fnimage  33385  imageval  33386  poimirlem4  34890  poimirlem5  34891  poimirlem6  34892  poimirlem7  34893  poimirlem8  34894  poimirlem9  34895  poimirlem10  34896  poimirlem11  34897  poimirlem12  34898  poimirlem13  34899  poimirlem14  34900  poimirlem15  34901  poimirlem16  34902  poimirlem17  34903  poimirlem18  34904  poimirlem19  34905  poimirlem20  34906  poimirlem21  34907  poimirlem22  34908  poimirlem25  34911  poimirlem26  34912  poimirlem27  34913  poimirlem29  34915  poimirlem31  34917  mblfinlem3  34925  mblfinlem4  34926  ismblfin  34927  itg2addnc  34940  sdclem2  35011  sdclem1  35012  heibor1lem  35081  glbconxN  36508  pmapglbx  36899  dvhb1dimN  38116  eldiophss  39364  setindtrs  39615  hbtlem2  39717  hbtlem5  39721  rngunsnply  39766  dftrcl3  40058  brtrclfv2  40065  dfrtrcl3  40071  dfhe3  40114  elscottab  40573  cpcolld  40587  nzss  40642  upbdrech  41565  fourierdlem36  42422  sge0resplit  42682  hoidmvlelem1  42871  elsprel  43631  opeliun2xp  44375  setrec2lem1  44790