Theorem elab 3632

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2144  {cab 2738  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835

This theorem is used by:  intab  4937  dfiun2g  4987  dfiin2g  4988  dfiunv2  4991  opeliunxp  5717  opeliun2xp  5718  dmopab2rex  5898  iotanul2  6511  elabrex  7246  abrexco  7248  uniuni  7776  finds  7908  finds2  7910  funcnvuni  7944  fiunlem  7954  fiun  7955  f1iun  7956  mapfset  8872  mapfoss  8874  fsetsspwxp  8875  mapval2  8900  sbthlem2  9107  ssenen  9170  dffi2  9415  dffi3  9423  tctr  9739  tcmin  9740  tc2  9741  tz9.13  9798  tcrank  9901  elscottab  9942  kardexOLD  9958  kardenOLD  9960  setrec2lem1  9974  cardf2  10024  cardiun  10063  alephval3  10189  dfac3  10200  dfac5lem3  10204  dfac5lem4  10205  dfac2b  10209  kmlem12  10240  cardcf  10329  cfeq0  10334  cfsuc  10335  cff1  10336  cflim2  10341  cfss  10343  axdc3lem2  10529  axdc3lem3  10530  axdclem  10597  brdom7disj  10610  brdom6disj  10611  tskuni  10868  gruina  10903  nqpr  11099  supadd  12285  supmul  12289  dfnn2  12348  dfuzi  12790  seqof  14202  hashfacen  14599  hashf1lem1  14600  hashf1lem2  14601  0csh0  14944  trclun  15167  dfrtrcl2  15215  shftfval  15223  infcvgaux1i  16026  sursubmefmnd  19092  injsubmefmnd  19093  smndex2dnrinv  19114  symg1bas  19605  pmtrprfvalrn  19702  psgnvali  19722  efgrelexlemb  19964  lss1d  21238  lidldvgen  21658  zndvds  21855  mpfind  22424  pf1ind  22673  cmpsublem  23717  cmpsub  23718  ptpjopn  23931  ptclsg  23934  txdis1cn  23954  tx1stc  23969  hauspwpwf1  24306  qustgplem  24440  ustn0  24540  i1fadd  26016  i1fmul  26017  i1fmulc  26024  nosupno  28060  nosupbnd1lem1  28065  noinfno  28075  addsproplem2  28356  addsproplem4  28358  addsproplem5  28359  addsproplem6  28360  addsuniflem  28387  negsid  28427  mulsproplem9  28510  mulsproplem12  28513  sltmuls1  28533  sltmuls2  28534  precsexlem9  28601  precsexlem11  28603  dfn0s2  28718  recut  28880  elreno2  28881  ausgrusgri  29749  ushgredgedg  29810  ushgredgedgloop  29812  wspniunwspnon  30512  rusgrnumwwlkb0  30563  fusgr2wsp2nb  30935  nmosetn0  31367  nmoolb  31373  nmlno0lem  31395  nmopsetn0  32467  nmfnsetn0  32480  nmoplb  32509  nmfnlb  32526  nmlnop0iALT  32597  nmopun  32616  nmcexi  32628  branmfn  32707  pjnmopi  32750  fpwrelmapffslem  33366  ldlfcntref  34528  esumc  34725  orvcval2  35133  onprcf1acwevdlem1  35937  derangenlem  35978  satfrnmapom  36177  fmlaomn0  36197  fmlasucdisj  36206  dmopab3rexdif  36212  2goelgoanfmla1  36231  mclsssvlem  36369  mclsind  36377  dfon2lem1  36587  dfon2lem3  36589  dfon2lem7  36593  fnimage  36733  imageval  36734  dfttc4  37360  poimirlem4  38585  poimirlem5  38586  poimirlem6  38587  poimirlem7  38588  poimirlem8  38589  poimirlem9  38590  poimirlem10  38591  poimirlem11  38592  poimirlem12  38593  poimirlem13  38594  poimirlem14  38595  poimirlem15  38596  poimirlem16  38597  poimirlem17  38598  poimirlem18  38599  poimirlem19  38600  poimirlem20  38601  poimirlem21  38602  poimirlem22  38603  poimirlem25  38606  poimirlem26  38607  poimirlem27  38608  poimirlem29  38610  poimirlem31  38612  mblfinlem3  38620  mblfinlem4  38621  ismblfin  38622  itg2addnc  38635  sdclem2  38719  sdclem1  38720  heibor1lem  38786  glbconxN  40478  pmapglbx  40869  dvhb1dimN  42086  sticksstones10  43248  sticksstones11  43249  sticksstones12a  43250  sticksstones12  43251  sticksstones17  43256  sticksstones18  43257  sticksstones19  43258  redvmptabs  43454  abbibw  43731  eldiophss  43828  setindtrs  44075  hbtlem2  44169  hbtlem5  44173  rngunsnply  44214  oaun3lem1  44419  oadif1lem  44424  oadif1  44425  dftrcl3  44763  brtrclfv2  44770  dfrtrcl3  44776  dfhe3  44818  cpcolld  45285  nzss  45344  upbdrech  46364  fourierdlem36  47196  sge0resplit  47459  hoidmvlelem1  47648  fsetsniunop  48162  elsprel  48600  ixpv  50041  iinfconstbas  50217