Theorem elab 3635

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {cab 2715  Vcvv 3441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812

This theorem is referenced by:  intab  4934  dfiun2g  4986  dfiin2g  4987  dfiunv2  4990  opeliunxp  5692  opeliun2xp  5693  dmopab2rex  5867  iotanul2  6466  elabrex  7191  abrexco  7193  uniuni  7710  finds  7841  finds2  7843  funcnvuni  7877  fiunlem  7889  fiun  7890  f1iun  7891  mapfset  8792  mapfoss  8794  fsetsspwxp  8795  mapval2  8815  sbthlem2  9021  ssenen  9084  dffi2  9331  dffi3  9339  tctr  9652  tcmin  9653  tc2  9654  tz9.13  9708  tcrank  9801  kardex  9811  karden  9812  cardf2  9860  cardiun  9899  alephval3  10025  dfac3  10036  dfac5lem3  10040  dfac5lem4  10041  dfac5lem4OLD  10043  dfac2b  10046  kmlem12  10077  cardcf  10167  cfeq0  10171  cfsuc  10172  cff1  10173  cflim2  10178  cfss  10180  axdc3lem2  10366  axdc3lem3  10367  axdclem  10434  brdom7disj  10446  brdom6disj  10447  tskuni  10699  gruina  10734  nqpr  10930  supadd  12115  supmul  12119  dfnn2  12163  dfuzi  12588  seqof  13987  hashfacen  14382  hashf1lem1  14383  hashf1lem2  14384  0csh0  14721  trclun  14942  dfrtrcl2  14990  shftfval  14998  infcvgaux1i  15785  sursubmefmnd  18826  injsubmefmnd  18827  smndex2dnrinv  18845  symg1bas  19325  pmtrprfvalrn  19422  psgnvali  19442  efgrelexlemb  19684  lss1d  20919  lidldvgen  21294  zndvds  21509  mpfind  22075  pf1ind  22304  cmpsublem  23348  cmpsub  23349  ptpjopn  23561  ptclsg  23564  txdis1cn  23584  tx1stc  23599  hauspwpwf1  23936  qustgplem  24070  ustn0  24170  i1fadd  25657  i1fmul  25658  i1fmulc  25665  nosupno  27676  nosupbnd1lem1  27681  noinfno  27691  addsproplem2  27971  addsproplem4  27973  addsproplem5  27974  addsproplem6  27975  addsuniflem  28002  negsid  28042  mulsproplem9  28125  mulsproplem12  28128  sltmuls1  28148  sltmuls2  28149  precsexlem9  28216  precsexlem11  28218  dfn0s2  28333  recut  28495  elreno2  28496  ausgrusgri  29246  ushgredgedg  29307  ushgredgedgloop  29309  wspniunwspnon  30001  rusgrnumwwlkb0  30052  fusgr2wsp2nb  30414  nmosetn0  30845  nmoolb  30851  nmlno0lem  30873  nmopsetn0  31945  nmfnsetn0  31958  nmoplb  31987  nmfnlb  32004  nmlnop0iALT  32075  nmopun  32094  nmcexi  32106  branmfn  32185  pjnmopi  32228  fpwrelmapffslem  32814  ldlfcntref  34024  esumc  34221  orvcval2  34629  derangenlem  35378  satfrnmapom  35577  fmlaomn0  35597  fmlasucdisj  35606  dmopab3rexdif  35612  2goelgoanfmla1  35631  mclsssvlem  35769  mclsind  35777  dfon2lem3  35990  dfon2lem7  35994  fnimage  36134  imageval  36135  poimirlem4  37838  poimirlem5  37839  poimirlem6  37840  poimirlem7  37841  poimirlem8  37842  poimirlem9  37843  poimirlem10  37844  poimirlem11  37845  poimirlem12  37846  poimirlem13  37847  poimirlem14  37848  poimirlem15  37849  poimirlem16  37850  poimirlem17  37851  poimirlem18  37852  poimirlem19  37853  poimirlem20  37854  poimirlem21  37855  poimirlem22  37856  poimirlem25  37859  poimirlem26  37860  poimirlem27  37861  poimirlem29  37863  poimirlem31  37865  mblfinlem3  37873  mblfinlem4  37874  ismblfin  37875  itg2addnc  37888  sdclem2  37956  sdclem1  37957  heibor1lem  38023  glbconxN  39717  pmapglbx  40108  dvhb1dimN  41325  sticksstones10  42488  sticksstones11  42489  sticksstones12a  42490  sticksstones12  42491  sticksstones17  42496  sticksstones18  42497  sticksstones19  42498  redvmptabs  42693  abbibw  42998  eldiophss  43094  setindtrs  43345  hbtlem2  43444  hbtlem5  43448  rngunsnply  43489  oaun3lem1  43694  oadif1lem  43699  oadif1  43700  dftrcl3  44039  brtrclfv2  44046  dfrtrcl3  44052  dfhe3  44094  elscottab  44563  cpcolld  44577  nzss  44636  upbdrech  45630  fourierdlem36  46464  sge0resplit  46727  hoidmvlelem1  46916  fsetsniunop  47372  elsprel  47798  ixpv  49212  iinfconstbas  49388  setrec2lem1  50015