Theorem elab 3629

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1550   ∈ wcel 2132  {cab 2730  Vcvv 3444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1553  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827

This theorem is referenced by:  intab  4926  dfiun2g  4977  dfiin2g  4978  dfiunv2  4981  opeliunxp  5703  opeliun2xp  5704  dmopab2rex  5882  iotanul2  6479  elabrex  7211  abrexco  7213  uniuni  7730  finds  7862  finds2  7864  funcnvuni  7898  fiunlem  7908  fiun  7909  f1iun  7910  mapfset  8816  mapfoss  8818  fsetsspwxp  8819  mapval2  8839  sbthlem2  9045  ssenen  9108  dffi2  9355  dffi3  9363  tctr  9679  tcmin  9680  tc2  9681  tz9.13  9735  tcrank  9828  kardex  9838  karden  9839  cardf2  9887  cardiun  9926  alephval3  10052  dfac3  10063  dfac5lem3  10067  dfac5lem4  10068  dfac5lem4OLD  10070  dfac2b  10073  kmlem12  10104  cardcf  10194  cfeq0  10199  cfsuc  10200  cff1  10201  cflim2  10206  cfss  10208  axdc3lem2  10394  axdc3lem3  10395  axdclem  10462  brdom7disj  10474  brdom6disj  10475  tskuni  10727  gruina  10762  nqpr  10958  supadd  12146  supmul  12150  dfnn2  12209  dfuzi  12650  seqof  14058  hashfacen  14453  hashf1lem1  14454  hashf1lem2  14455  0csh0  14792  trclun  15013  dfrtrcl2  15061  shftfval  15069  infcvgaux1i  15859  sursubmefmnd  18902  injsubmefmnd  18903  smndex2dnrinv  18924  symg1bas  19403  pmtrprfvalrn  19500  psgnvali  19520  efgrelexlemb  19762  lss1d  20999  lidldvgen  21373  zndvds  21570  mpfind  22137  pf1ind  22387  cmpsublem  23428  cmpsub  23429  ptpjopn  23641  ptclsg  23644  txdis1cn  23664  tx1stc  23679  hauspwpwf1  24016  qustgplem  24150  ustn0  24250  i1fadd  25726  i1fmul  25727  i1fmulc  25734  nosupno  27733  nosupbnd1lem1  27738  noinfno  27748  addsproplem2  28029  addsproplem4  28031  addsproplem5  28032  addsproplem6  28033  addsuniflem  28060  negsid  28100  mulsproplem9  28183  mulsproplem12  28186  sltmuls1  28206  sltmuls2  28207  precsexlem9  28274  precsexlem11  28276  dfn0s2  28391  recut  28553  elreno2  28554  ausgrusgri  29304  ushgredgedg  29365  ushgredgedgloop  29367  wspniunwspnon  30058  rusgrnumwwlkb0  30109  fusgr2wsp2nb  30471  nmosetn0  30903  nmoolb  30909  nmlno0lem  30931  nmopsetn0  32003  nmfnsetn0  32016  nmoplb  32045  nmfnlb  32062  nmlnop0iALT  32133  nmopun  32152  nmcexi  32164  branmfn  32243  pjnmopi  32286  fpwrelmapffslem  32873  ldlfcntref  34095  esumc  34292  orvcval2  34700  derangenlem  35459  satfrnmapom  35658  fmlaomn0  35678  fmlasucdisj  35687  dmopab3rexdif  35693  2goelgoanfmla1  35712  mclsssvlem  35850  mclsind  35858  dfon2lem3  36071  dfon2lem7  36075  fnimage  36215  imageval  36216  dfttc4  36828  poimirlem4  38061  poimirlem5  38062  poimirlem6  38063  poimirlem7  38064  poimirlem8  38065  poimirlem9  38066  poimirlem10  38067  poimirlem11  38068  poimirlem12  38069  poimirlem13  38070  poimirlem14  38071  poimirlem15  38072  poimirlem16  38073  poimirlem17  38074  poimirlem18  38075  poimirlem19  38076  poimirlem20  38077  poimirlem21  38078  poimirlem22  38079  poimirlem25  38082  poimirlem26  38083  poimirlem27  38084  poimirlem29  38086  poimirlem31  38088  mblfinlem3  38096  mblfinlem4  38097  ismblfin  38098  itg2addnc  38111  sdclem2  38179  sdclem1  38180  heibor1lem  38246  glbconxN  39940  pmapglbx  40331  dvhb1dimN  41548  sticksstones10  42710  sticksstones11  42711  sticksstones12a  42712  sticksstones12  42713  sticksstones17  42718  sticksstones18  42719  sticksstones19  42720  redvmptabs  42907  abbibw  43197  eldiophss  43293  setindtrs  43540  hbtlem2  43639  hbtlem5  43643  rngunsnply  43684  oaun3lem1  43889  oadif1lem  43894  oadif1  43895  dftrcl3  44234  brtrclfv2  44241  dfrtrcl3  44247  dfhe3  44289  elscottab  44758  cpcolld  44772  nzss  44831  upbdrech  45822  fourierdlem36  46655  sge0resplit  46918  hoidmvlelem1  47107  fsetsniunop  47581  elsprel  48019  ixpv  49449  iinfconstbas  49625  setrec2lem1  50252