Theorem elab 3646

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {cab 2707  Vcvv 3447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803

This theorem is referenced by:  intab  4942  dfiun2g  4994  dfiin2g  4996  dfiunv2  4999  opeliunxp  5705  opeliun2xp  5706  dmopab2rex  5881  iotanul2  6481  elabrex  7216  abrexco  7218  uniuni  7738  finds  7872  finds2  7874  funcnvuni  7908  fiunlem  7920  fiun  7921  f1iun  7922  mapfset  8823  mapfoss  8825  fsetsspwxp  8826  mapval2  8845  sbthlem2  9052  ssenen  9115  dffi2  9374  dffi3  9382  tctr  9693  tcmin  9694  tc2  9695  tz9.13  9744  tcrank  9837  kardex  9847  karden  9848  cardf2  9896  cardiun  9935  alephval3  10063  dfac3  10074  dfac5lem3  10078  dfac5lem4  10079  dfac5lem4OLD  10081  dfac2b  10084  kmlem12  10115  cardcf  10205  cfeq0  10209  cfsuc  10210  cff1  10211  cflim2  10216  cfss  10218  axdc3lem2  10404  axdc3lem3  10405  axdclem  10472  brdom7disj  10484  brdom6disj  10485  tskuni  10736  gruina  10771  nqpr  10967  supadd  12151  supmul  12155  dfnn2  12199  dfuzi  12625  seqof  14024  hashfacen  14419  hashf1lem1  14420  hashf1lem2  14421  0csh0  14758  trclun  14980  dfrtrcl2  15028  shftfval  15036  infcvgaux1i  15823  sursubmefmnd  18823  injsubmefmnd  18824  smndex2dnrinv  18842  symg1bas  19321  pmtrprfvalrn  19418  psgnvali  19438  efgrelexlemb  19680  lss1d  20869  lidldvgen  21244  zndvds  21459  mpfind  22014  pf1ind  22242  cmpsublem  23286  cmpsub  23287  ptpjopn  23499  ptclsg  23502  txdis1cn  23522  tx1stc  23537  hauspwpwf1  23874  qustgplem  24008  ustn0  24108  i1fadd  25596  i1fmul  25597  i1fmulc  25604  nosupno  27615  nosupbnd1lem1  27620  noinfno  27630  addsproplem2  27877  addsproplem4  27879  addsproplem5  27880  addsproplem6  27881  addsuniflem  27908  negsid  27947  mulsproplem9  28027  mulsproplem12  28030  ssltmul1  28050  ssltmul2  28051  precsexlem9  28117  precsexlem11  28119  dfn0s2  28224  recut  28347  0reno  28348  ausgrusgri  29095  ushgredgedg  29156  ushgredgedgloop  29158  wspniunwspnon  29853  rusgrnumwwlkb0  29901  fusgr2wsp2nb  30263  nmosetn0  30694  nmoolb  30700  nmlno0lem  30722  nmopsetn0  31794  nmfnsetn0  31807  nmoplb  31836  nmfnlb  31853  nmlnop0iALT  31924  nmopun  31943  nmcexi  31955  branmfn  32034  pjnmopi  32077  fpwrelmapffslem  32655  ldlfcntref  33844  esumc  34041  orvcval2  34450  derangenlem  35158  satfrnmapom  35357  fmlaomn0  35377  fmlasucdisj  35386  dmopab3rexdif  35392  2goelgoanfmla1  35411  mclsssvlem  35549  mclsind  35557  dfon2lem3  35773  dfon2lem7  35777  fnimage  35917  imageval  35918  poimirlem4  37618  poimirlem5  37619  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem9  37623  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem13  37627  poimirlem14  37628  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem18  37632  poimirlem19  37633  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  poimirlem29  37643  poimirlem31  37645  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  itg2addnc  37668  sdclem2  37736  sdclem1  37737  heibor1lem  37803  glbconxN  39372  pmapglbx  39763  dvhb1dimN  40980  sticksstones10  42143  sticksstones11  42144  sticksstones12a  42145  sticksstones12  42146  sticksstones17  42151  sticksstones18  42152  sticksstones19  42153  redvmptabs  42348  abbibw  42665  eldiophss  42762  setindtrs  43014  hbtlem2  43113  hbtlem5  43117  rngunsnply  43158  oaun3lem1  43363  oadif1lem  43368  oadif1  43369  dftrcl3  43709  brtrclfv2  43716  dfrtrcl3  43722  dfhe3  43764  elscottab  44233  cpcolld  44247  nzss  44306  upbdrech  45303  fourierdlem36  46141  sge0resplit  46404  hoidmvlelem1  46593  fsetsniunop  47050  elsprel  47476  ixpv  48878  iinfconstbas  49055  setrec2lem1  49682