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 2175, ax-11 2191, ax-12 2212. (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 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2142  {cab 2740  Vcvv 3454

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837

This theorem is used by:  intab  4942  dfiun2g  4993  dfiin2g  4994  dfiunv2  4997  opeliunxp  5727  opeliun2xp  5728  dmopab2rex  5906  iotanul2  6509  elabrex  7240  abrexco  7242  uniuni  7759  finds  7891  finds2  7893  funcnvuni  7927  fiunlem  7937  fiun  7938  f1iun  7939  mapfset  8845  mapfoss  8847  fsetsspwxp  8848  mapval2  8868  sbthlem2  9074  ssenen  9137  dffi2  9381  dffi3  9389  tctr  9705  tcmin  9706  tc2  9707  tz9.13  9761  tcrank  9854  elscottab  9869  kardexOLD  9885  kardenOLD  9887  cardf2  9936  cardiun  9975  alephval3  10101  dfac3  10112  dfac5lem3  10116  dfac5lem4  10117  dfac2b  10121  kmlem12  10152  cardcf  10241  cfeq0  10246  cfsuc  10247  cff1  10248  cflim2  10253  cfss  10255  axdc3lem2  10441  axdc3lem3  10442  axdclem  10509  brdom7disj  10521  brdom6disj  10522  tskuni  10774  gruina  10809  nqpr  11005  supadd  12189  supmul  12193  dfnn2  12252  dfuzi  12693  seqof  14102  hashfacen  14498  hashf1lem1  14499  hashf1lem2  14500  0csh0  14837  trclun  15058  dfrtrcl2  15106  shftfval  15114  infcvgaux1i  15918  sursubmefmnd  18961  injsubmefmnd  18962  smndex2dnrinv  18983  symg1bas  19467  pmtrprfvalrn  19564  psgnvali  19584  efgrelexlemb  19826  lss1d  21095  lidldvgen  21513  zndvds  21710  mpfind  22277  pf1ind  22526  cmpsublem  23567  cmpsub  23568  ptpjopn  23780  ptclsg  23783  txdis1cn  23803  tx1stc  23818  hauspwpwf1  24155  qustgplem  24289  ustn0  24389  i1fadd  25865  i1fmul  25866  i1fmulc  25873  nosupno  27878  nosupbnd1lem1  27883  noinfno  27893  addsproplem2  28174  addsproplem4  28176  addsproplem5  28177  addsproplem6  28178  addsuniflem  28205  negsid  28245  mulsproplem9  28328  mulsproplem12  28331  sltmuls1  28351  sltmuls2  28352  precsexlem9  28419  precsexlem11  28421  dfn0s2  28536  recut  28698  elreno2  28699  ausgrusgri  29529  ushgredgedg  29590  ushgredgedgloop  29592  wspniunwspnon  30283  rusgrnumwwlkb0  30334  fusgr2wsp2nb  30696  nmosetn0  31128  nmoolb  31134  nmlno0lem  31156  nmopsetn0  32228  nmfnsetn0  32241  nmoplb  32270  nmfnlb  32287  nmlnop0iALT  32358  nmopun  32377  nmcexi  32389  branmfn  32468  pjnmopi  32511  fpwrelmapffslem  33088  ldlfcntref  34253  esumc  34450  orvcval2  34858  derangenlem  35671  satfrnmapom  35870  fmlaomn0  35890  fmlasucdisj  35899  dmopab3rexdif  35905  2goelgoanfmla1  35924  mclsssvlem  36062  mclsind  36070  dfon2lem3  36283  dfon2lem7  36287  fnimage  36427  imageval  36428  dfttc4  37069  poimirlem4  38303  poimirlem5  38304  poimirlem6  38305  poimirlem7  38306  poimirlem8  38307  poimirlem9  38308  poimirlem10  38309  poimirlem11  38310  poimirlem12  38311  poimirlem13  38312  poimirlem14  38313  poimirlem15  38314  poimirlem16  38315  poimirlem17  38316  poimirlem18  38317  poimirlem19  38318  poimirlem20  38319  poimirlem21  38320  poimirlem22  38321  poimirlem25  38324  poimirlem26  38325  poimirlem27  38326  poimirlem29  38328  poimirlem31  38330  mblfinlem3  38338  mblfinlem4  38339  ismblfin  38340  itg2addnc  38353  sdclem2  38421  sdclem1  38422  heibor1lem  38488  glbconxN  40180  pmapglbx  40571  dvhb1dimN  41788  sticksstones10  42950  sticksstones11  42951  sticksstones12a  42952  sticksstones12  42953  sticksstones17  42958  sticksstones18  42959  sticksstones19  42960  redvmptabs  43149  abbibw  43437  eldiophss  43533  setindtrs  43780  hbtlem2  43879  hbtlem5  43883  rngunsnply  43924  oaun3lem1  44129  oadif1lem  44134  oadif1  44135  dftrcl3  44474  brtrclfv2  44481  dfrtrcl3  44487  dfhe3  44529  cpcolld  44996  nzss  45055  upbdrech  46052  fourierdlem36  46885  sge0resplit  47148  hoidmvlelem1  47337  fsetsniunop  47814  elsprel  48252  ixpv  49696  iinfconstbas  49872  setrec2lem1  50499