Theorem elab 3633

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2110  {cab 2708  Vcvv 3434

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804

This theorem is referenced by:  intab  4926  dfiun2g  4978  dfiin2g  4979  dfiunv2  4982  opeliunxp  5681  opeliun2xp  5682  dmopab2rex  5855  iotanul2  6450  elabrex  7171  abrexco  7173  uniuni  7690  finds  7821  finds2  7823  funcnvuni  7857  fiunlem  7869  fiun  7870  f1iun  7871  mapfset  8769  mapfoss  8771  fsetsspwxp  8772  mapval2  8791  sbthlem2  8996  ssenen  9059  dffi2  9302  dffi3  9310  tctr  9625  tcmin  9626  tc2  9627  tz9.13  9676  tcrank  9769  kardex  9779  karden  9780  cardf2  9828  cardiun  9867  alephval3  9993  dfac3  10004  dfac5lem3  10008  dfac5lem4  10009  dfac5lem4OLD  10011  dfac2b  10014  kmlem12  10045  cardcf  10135  cfeq0  10139  cfsuc  10140  cff1  10141  cflim2  10146  cfss  10148  axdc3lem2  10334  axdc3lem3  10335  axdclem  10402  brdom7disj  10414  brdom6disj  10415  tskuni  10666  gruina  10701  nqpr  10897  supadd  12082  supmul  12086  dfnn2  12130  dfuzi  12556  seqof  13958  hashfacen  14353  hashf1lem1  14354  hashf1lem2  14355  0csh0  14692  trclun  14913  dfrtrcl2  14961  shftfval  14969  infcvgaux1i  15756  sursubmefmnd  18796  injsubmefmnd  18797  smndex2dnrinv  18815  symg1bas  19296  pmtrprfvalrn  19393  psgnvali  19413  efgrelexlemb  19655  lss1d  20889  lidldvgen  21264  zndvds  21479  mpfind  22035  pf1ind  22263  cmpsublem  23307  cmpsub  23308  ptpjopn  23520  ptclsg  23523  txdis1cn  23543  tx1stc  23558  hauspwpwf1  23895  qustgplem  24029  ustn0  24129  i1fadd  25616  i1fmul  25617  i1fmulc  25624  nosupno  27635  nosupbnd1lem1  27640  noinfno  27650  addsproplem2  27906  addsproplem4  27908  addsproplem5  27909  addsproplem6  27910  addsuniflem  27937  negsid  27976  mulsproplem9  28056  mulsproplem12  28059  ssltmul1  28079  ssltmul2  28080  precsexlem9  28146  precsexlem11  28148  dfn0s2  28253  recut  28391  0reno  28392  ausgrusgri  29139  ushgredgedg  29200  ushgredgedgloop  29202  wspniunwspnon  29894  rusgrnumwwlkb0  29942  fusgr2wsp2nb  30304  nmosetn0  30735  nmoolb  30741  nmlno0lem  30763  nmopsetn0  31835  nmfnsetn0  31848  nmoplb  31877  nmfnlb  31894  nmlnop0iALT  31965  nmopun  31984  nmcexi  31996  branmfn  32075  pjnmopi  32118  fpwrelmapffslem  32705  ldlfcntref  33857  esumc  34054  orvcval2  34462  derangenlem  35183  satfrnmapom  35382  fmlaomn0  35402  fmlasucdisj  35411  dmopab3rexdif  35417  2goelgoanfmla1  35436  mclsssvlem  35574  mclsind  35582  dfon2lem3  35798  dfon2lem7  35802  fnimage  35942  imageval  35943  poimirlem4  37643  poimirlem5  37644  poimirlem6  37645  poimirlem7  37646  poimirlem8  37647  poimirlem9  37648  poimirlem10  37649  poimirlem11  37650  poimirlem12  37651  poimirlem13  37652  poimirlem14  37653  poimirlem15  37654  poimirlem16  37655  poimirlem17  37656  poimirlem18  37657  poimirlem19  37658  poimirlem20  37659  poimirlem21  37660  poimirlem22  37661  poimirlem25  37664  poimirlem26  37665  poimirlem27  37666  poimirlem29  37668  poimirlem31  37670  mblfinlem3  37678  mblfinlem4  37679  ismblfin  37680  itg2addnc  37693  sdclem2  37761  sdclem1  37762  heibor1lem  37828  glbconxN  39396  pmapglbx  39787  dvhb1dimN  41004  sticksstones10  42167  sticksstones11  42168  sticksstones12a  42169  sticksstones12  42170  sticksstones17  42175  sticksstones18  42176  sticksstones19  42177  redvmptabs  42372  abbibw  42689  eldiophss  42786  setindtrs  43037  hbtlem2  43136  hbtlem5  43140  rngunsnply  43181  oaun3lem1  43386  oadif1lem  43391  oadif1  43392  dftrcl3  43732  brtrclfv2  43739  dfrtrcl3  43745  dfhe3  43787  elscottab  44256  cpcolld  44270  nzss  44329  upbdrech  45325  fourierdlem36  46160  sge0resplit  46423  hoidmvlelem1  46612  fsetsniunop  47059  elsprel  47485  ixpv  48900  iinfconstbas  49077  setrec2lem1  49704