Theorem elab 3681

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2106  {cab 2712  Vcvv 3478

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 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814

This theorem is referenced by:  ralabOLD  3701  rexabOLD  3704  intab  4983  dfiun2g  5035  dfiin2g  5037  dfiunv2  5040  opeliunxp  5756  dmopab2rex  5931  iotanul2  6533  elabrex  7262  abrexco  7264  uniuni  7781  finds  7919  finds2  7921  funcnvuni  7955  fiunlem  7965  fiun  7966  f1iun  7967  mapfset  8889  mapfoss  8891  fsetsspwxp  8892  mapval2  8911  sbthlem2  9123  ssenen  9190  dffi2  9461  dffi3  9469  tctr  9778  tcmin  9779  tc2  9780  tz9.13  9829  tcrank  9922  kardex  9932  karden  9933  cardf2  9981  cardiun  10020  alephval3  10148  dfac3  10159  dfac5lem3  10163  dfac5lem4  10164  dfac5lem4OLD  10166  dfac2b  10169  kmlem12  10200  cardcf  10290  cfeq0  10294  cfsuc  10295  cff1  10296  cflim2  10301  cfss  10303  axdc3lem2  10489  axdc3lem3  10490  axdclem  10557  brdom7disj  10569  brdom6disj  10570  tskuni  10821  gruina  10856  nqpr  11052  supadd  12234  supmul  12238  dfnn2  12277  dfuzi  12707  seqof  14097  hashfacen  14490  hashf1lem1  14491  hashf1lem2  14492  0csh0  14828  trclun  15050  dfrtrcl2  15098  shftfval  15106  infcvgaux1i  15890  sursubmefmnd  18922  injsubmefmnd  18923  smndex2dnrinv  18941  symg1bas  19423  pmtrprfvalrn  19521  psgnvali  19541  efgrelexlemb  19783  lss1d  20979  lidldvgen  21362  zndvds  21586  mpfind  22149  pf1ind  22375  cmpsublem  23423  cmpsub  23424  ptpjopn  23636  ptclsg  23639  txdis1cn  23659  tx1stc  23674  hauspwpwf1  24011  qustgplem  24145  ustn0  24245  i1fadd  25744  i1fmul  25745  i1fmulc  25753  nosupno  27763  nosupbnd1lem1  27768  noinfno  27778  addsproplem2  28018  addsproplem4  28020  addsproplem5  28021  addsproplem6  28022  addsuniflem  28049  negsid  28088  mulsproplem9  28165  mulsproplem12  28168  ssltmul1  28188  ssltmul2  28189  precsexlem9  28254  precsexlem11  28256  dfn0s2  28351  recut  28443  0reno  28444  ausgrusgri  29200  ushgredgedg  29261  ushgredgedgloop  29263  wspniunwspnon  29953  rusgrnumwwlkb0  30001  fusgr2wsp2nb  30363  nmosetn0  30794  nmoolb  30800  nmlno0lem  30822  nmopsetn0  31894  nmfnsetn0  31907  nmoplb  31936  nmfnlb  31953  nmlnop0iALT  32024  nmopun  32043  nmcexi  32055  branmfn  32134  pjnmopi  32177  fpwrelmapffslem  32750  ldlfcntref  33815  esumc  34032  orvcval2  34440  derangenlem  35156  satfrnmapom  35355  fmlaomn0  35375  fmlasucdisj  35384  dmopab3rexdif  35390  2goelgoanfmla1  35409  mclsssvlem  35547  mclsind  35555  dfon2lem3  35767  dfon2lem7  35771  fnimage  35911  imageval  35912  poimirlem4  37611  poimirlem5  37612  poimirlem6  37613  poimirlem7  37614  poimirlem8  37615  poimirlem9  37616  poimirlem10  37617  poimirlem11  37618  poimirlem12  37619  poimirlem13  37620  poimirlem14  37621  poimirlem15  37622  poimirlem16  37623  poimirlem17  37624  poimirlem18  37625  poimirlem19  37626  poimirlem20  37627  poimirlem21  37628  poimirlem22  37629  poimirlem25  37632  poimirlem26  37633  poimirlem27  37634  poimirlem29  37636  poimirlem31  37638  mblfinlem3  37646  mblfinlem4  37647  ismblfin  37648  itg2addnc  37661  sdclem2  37729  sdclem1  37730  heibor1lem  37796  glbconxN  39361  pmapglbx  39752  dvhb1dimN  40969  sticksstones10  42137  sticksstones11  42138  sticksstones12a  42139  sticksstones12  42140  sticksstones17  42145  sticksstones18  42146  sticksstones19  42147  redvmptabs  42369  abbibw  42664  eldiophss  42762  setindtrs  43014  hbtlem2  43113  hbtlem5  43117  rngunsnply  43158  oaun3lem1  43364  oadif1lem  43369  oadif1  43370  dftrcl3  43710  brtrclfv2  43717  dfrtrcl3  43723  dfhe3  43765  elscottab  44240  cpcolld  44254  nzss  44313  upbdrech  45256  fourierdlem36  46099  sge0resplit  46362  hoidmvlelem1  46551  fsetsniunop  46999  elsprel  47400  opeliun2xp  48178  setrec2lem1  48924