Theorem elab 3637

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 2142, ax-11 2158, ax-12 2178. (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 3634	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
4	1, 3	ax-mp 5	1 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {cab 2707  Vcvv 3438

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803

This theorem is referenced by:  intab  4931  dfiun2g  4983  dfiin2g  4984  dfiunv2  4987  opeliunxp  5690  opeliun2xp  5691  dmopab2rex  5864  iotanul2  6459  elabrex  7182  abrexco  7184  uniuni  7702  finds  7836  finds2  7838  funcnvuni  7872  fiunlem  7884  fiun  7885  f1iun  7886  mapfset  8784  mapfoss  8786  fsetsspwxp  8787  mapval2  8806  sbthlem2  9012  ssenen  9075  dffi2  9332  dffi3  9340  tctr  9655  tcmin  9656  tc2  9657  tz9.13  9706  tcrank  9799  kardex  9809  karden  9810  cardf2  9858  cardiun  9897  alephval3  10023  dfac3  10034  dfac5lem3  10038  dfac5lem4  10039  dfac5lem4OLD  10041  dfac2b  10044  kmlem12  10075  cardcf  10165  cfeq0  10169  cfsuc  10170  cff1  10171  cflim2  10176  cfss  10178  axdc3lem2  10364  axdc3lem3  10365  axdclem  10432  brdom7disj  10444  brdom6disj  10445  tskuni  10696  gruina  10731  nqpr  10927  supadd  12111  supmul  12115  dfnn2  12159  dfuzi  12585  seqof  13984  hashfacen  14379  hashf1lem1  14380  hashf1lem2  14381  0csh0  14717  trclun  14939  dfrtrcl2  14987  shftfval  14995  infcvgaux1i  15782  sursubmefmnd  18788  injsubmefmnd  18789  smndex2dnrinv  18807  symg1bas  19288  pmtrprfvalrn  19385  psgnvali  19405  efgrelexlemb  19647  lss1d  20884  lidldvgen  21259  zndvds  21474  mpfind  22030  pf1ind  22258  cmpsublem  23302  cmpsub  23303  ptpjopn  23515  ptclsg  23518  txdis1cn  23538  tx1stc  23553  hauspwpwf1  23890  qustgplem  24024  ustn0  24124  i1fadd  25612  i1fmul  25613  i1fmulc  25620  nosupno  27631  nosupbnd1lem1  27636  noinfno  27646  addsproplem2  27900  addsproplem4  27902  addsproplem5  27903  addsproplem6  27904  addsuniflem  27931  negsid  27970  mulsproplem9  28050  mulsproplem12  28053  ssltmul1  28073  ssltmul2  28074  precsexlem9  28140  precsexlem11  28142  dfn0s2  28247  recut  28383  0reno  28384  ausgrusgri  29131  ushgredgedg  29192  ushgredgedgloop  29194  wspniunwspnon  29886  rusgrnumwwlkb0  29934  fusgr2wsp2nb  30296  nmosetn0  30727  nmoolb  30733  nmlno0lem  30755  nmopsetn0  31827  nmfnsetn0  31840  nmoplb  31869  nmfnlb  31886  nmlnop0iALT  31957  nmopun  31976  nmcexi  31988  branmfn  32067  pjnmopi  32110  fpwrelmapffslem  32688  ldlfcntref  33820  esumc  34017  orvcval2  34426  derangenlem  35143  satfrnmapom  35342  fmlaomn0  35362  fmlasucdisj  35371  dmopab3rexdif  35377  2goelgoanfmla1  35396  mclsssvlem  35534  mclsind  35542  dfon2lem3  35758  dfon2lem7  35762  fnimage  35902  imageval  35903  poimirlem4  37603  poimirlem5  37604  poimirlem6  37605  poimirlem7  37606  poimirlem8  37607  poimirlem9  37608  poimirlem10  37609  poimirlem11  37610  poimirlem12  37611  poimirlem13  37612  poimirlem14  37613  poimirlem15  37614  poimirlem16  37615  poimirlem17  37616  poimirlem18  37617  poimirlem19  37618  poimirlem20  37619  poimirlem21  37620  poimirlem22  37621  poimirlem25  37624  poimirlem26  37625  poimirlem27  37626  poimirlem29  37628  poimirlem31  37630  mblfinlem3  37638  mblfinlem4  37639  ismblfin  37640  itg2addnc  37653  sdclem2  37721  sdclem1  37722  heibor1lem  37788  glbconxN  39357  pmapglbx  39748  dvhb1dimN  40965  sticksstones10  42128  sticksstones11  42129  sticksstones12a  42130  sticksstones12  42131  sticksstones17  42136  sticksstones18  42137  sticksstones19  42138  redvmptabs  42333  abbibw  42650  eldiophss  42747  setindtrs  42998  hbtlem2  43097  hbtlem5  43101  rngunsnply  43142  oaun3lem1  43347  oadif1lem  43352  oadif1  43353  dftrcl3  43693  brtrclfv2  43700  dfrtrcl3  43706  dfhe3  43748  elscottab  44217  cpcolld  44231  nzss  44290  upbdrech  45287  fourierdlem36  46125  sge0resplit  46388  hoidmvlelem1  46577  fsetsniunop  47034  elsprel  47460  ixpv  48862  iinfconstbas  49039  setrec2lem1  49666