Theorem elab 3636

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2147  {cab 2741  Vcvv 3454

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839

This theorem is used by:  intab  4941  dfiun2g  4991  dfiin2g  4992  dfiunv2  4995  opeliunxp  5722  opeliun2xp  5723  dmopab2rex  5906  iotanul2  6529  elabrex  7269  abrexco  7271  uniuni  7800  finds  7932  finds2  7934  funcnvuni  7968  fiunlem  7978  fiun  7979  f1iun  7980  mapfset  8900  mapfoss  8902  fsetsspwxp  8903  mapval2  8928  sbthlem2  9135  ssenen  9198  dffi2  9442  dffi3  9450  tctr  9766  tcmin  9767  tc2  9768  tz9.13  9825  tcrank  9928  elscottab  9969  kardexOLD  9985  kardenOLD  9987  setrec2lem1  10001  cardf2  10051  cardiun  10090  alephval3  10216  dfac3  10227  dfac5lem3  10231  dfac5lem4  10232  dfac2b  10236  kmlem12  10267  cardcf  10356  cfeq0  10361  cfsuc  10362  cff1  10363  cflim2  10368  cfss  10370  axdc3lem2  10556  axdc3lem3  10557  axdclem  10624  brdom7disj  10637  brdom6disj  10638  tskuni  10895  gruina  10930  nqpr  11126  supadd  12312  supmul  12316  dfnn2  12375  dfuzi  12817  seqof  14229  hashfacen  14626  hashf1lem1  14627  hashf1lem2  14628  0csh0  14972  trclun  15196  dfrtrcl2  15244  shftfval  15252  infcvgaux1i  16055  sursubmefmnd  19121  injsubmefmnd  19122  smndex2dnrinv  19143  symg1bas  19635  pmtrprfvalrn  19732  psgnvali  19752  efgrelexlemb  19994  lss1d  21268  lidldvgen  21688  zndvds  21885  mpfind  22454  pf1ind  22703  cmpsublem  23747  cmpsub  23748  ptpjopn  23961  ptclsg  23964  txdis1cn  23984  tx1stc  23999  hauspwpwf1  24336  qustgplem  24470  ustn0  24570  i1fadd  26046  i1fmul  26047  i1fmulc  26054  nosupno  28090  nosupbnd1lem1  28095  noinfno  28105  addsproplem2  28386  addsproplem4  28388  addsproplem5  28389  addsproplem6  28390  addsuniflem  28417  negsid  28457  mulsproplem9  28540  mulsproplem12  28543  sltmuls1  28563  sltmuls2  28564  precsexlem9  28631  precsexlem11  28633  dfn0s2  28748  recut  28910  elreno2  28911  ausgrusgri  29779  ushgredgedg  29840  ushgredgedgloop  29842  wspniunwspnon  30542  rusgrnumwwlkb0  30593  fusgr2wsp2nb  30965  nmosetn0  31397  nmoolb  31403  nmlno0lem  31425  nmopsetn0  32497  nmfnsetn0  32510  nmoplb  32539  nmfnlb  32556  nmlnop0iALT  32627  nmopun  32646  nmcexi  32658  branmfn  32737  pjnmopi  32780  fpwrelmapffslem  33394  ldlfcntref  34556  esumc  34753  orvcval2  35161  onprcf1acwevdlem1  36045  derangenlem  36103  satfrnmapom  36302  fmlaomn0  36322  fmlasucdisj  36331  dmopab3rexdif  36337  2goelgoanfmla1  36356  mclsssvlem  36494  mclsind  36502  dfon2lem1  36723  dfon2lem3  36725  dfon2lem7  36729  fnimage  36869  imageval  36870  dfttc4  37496  poimirlem4  38734  poimirlem5  38735  poimirlem6  38736  poimirlem7  38737  poimirlem8  38738  poimirlem9  38739  poimirlem10  38740  poimirlem11  38741  poimirlem12  38742  poimirlem13  38743  poimirlem14  38744  poimirlem15  38745  poimirlem16  38746  poimirlem17  38747  poimirlem18  38748  poimirlem19  38749  poimirlem20  38750  poimirlem21  38751  poimirlem22  38752  poimirlem25  38755  poimirlem26  38756  poimirlem27  38757  poimirlem29  38759  poimirlem31  38761  mblfinlem3  38769  mblfinlem4  38770  ismblfin  38771  itg2addnc  38784  sdclem2  38868  sdclem1  38869  heibor1lem  38935  glbconxN  40627  pmapglbx  41018  dvhb1dimN  42235  sticksstones10  43397  sticksstones11  43398  sticksstones12a  43399  sticksstones12  43400  sticksstones17  43405  sticksstones18  43406  sticksstones19  43407  redvmptabs  43604  abbibw  43881  eldiophss  43978  setindtrs  44225  hbtlem2  44318  hbtlem5  44322  rngunsnply  44363  oaun3lem1  44568  oadif1lem  44573  oadif1  44574  dftrcl3  44912  brtrclfv2  44919  dfrtrcl3  44925  dfhe3  44967  cpcolld  45434  nzss  45493  upbdrech  46526  fourierdlem36  47358  sge0resplit  47621  hoidmvlelem1  47810  fsetsniunop  48324  elsprel  48762  ixpv  50208  iinfconstbas  50385