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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1568   ∈ wcel 2141  {cab 2739  Vcvv 3453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836

This theorem is referenced by:  intab  4942  dfiun2g  4993  dfiin2g  4994  dfiunv2  4997  opeliunxp  5728  opeliun2xp  5729  dmopab2rex  5907  iotanul2  6509  elabrex  7240  abrexco  7242  uniuni  7760  finds  7892  finds2  7894  funcnvuni  7928  fiunlem  7938  fiun  7939  f1iun  7940  mapfset  8846  mapfoss  8848  fsetsspwxp  8849  mapval2  8869  sbthlem2  9075  ssenen  9138  dffi2  9382  dffi3  9390  tctr  9706  tcmin  9707  tc2  9708  tz9.13  9762  tcrank  9855  elscottab  9869  kardex  9879  karden  9880  cardf2  9928  cardiun  9967  alephval3  10093  dfac3  10104  dfac5lem3  10108  dfac5lem4  10109  dfac2b  10113  kmlem12  10144  cardcf  10234  cfeq0  10239  cfsuc  10240  cff1  10241  cflim2  10246  cfss  10248  axdc3lem2  10434  axdc3lem3  10435  axdclem  10502  brdom7disj  10514  brdom6disj  10515  tskuni  10767  gruina  10802  nqpr  10998  supadd  12182  supmul  12186  dfnn2  12245  dfuzi  12686  seqof  14094  hashfacen  14490  hashf1lem1  14491  hashf1lem2  14492  0csh0  14829  trclun  15050  dfrtrcl2  15098  shftfval  15106  infcvgaux1i  15910  sursubmefmnd  18954  injsubmefmnd  18955  smndex2dnrinv  18976  symg1bas  19460  pmtrprfvalrn  19557  psgnvali  19577  efgrelexlemb  19819  lss1d  21063  lidldvgen  21481  zndvds  21678  mpfind  22245  pf1ind  22494  cmpsublem  23535  cmpsub  23536  ptpjopn  23748  ptclsg  23751  txdis1cn  23771  tx1stc  23786  hauspwpwf1  24123  qustgplem  24257  ustn0  24357  i1fadd  25833  i1fmul  25834  i1fmulc  25841  nosupno  27843  nosupbnd1lem1  27848  noinfno  27858  addsproplem2  28139  addsproplem4  28141  addsproplem5  28142  addsproplem6  28143  addsuniflem  28170  negsid  28210  mulsproplem9  28293  mulsproplem12  28296  sltmuls1  28316  sltmuls2  28317  precsexlem9  28384  precsexlem11  28386  dfn0s2  28501  recut  28663  elreno2  28664  ausgrusgri  29484  ushgredgedg  29545  ushgredgedgloop  29547  wspniunwspnon  30238  rusgrnumwwlkb0  30289  fusgr2wsp2nb  30651  nmosetn0  31083  nmoolb  31089  nmlno0lem  31111  nmopsetn0  32183  nmfnsetn0  32196  nmoplb  32225  nmfnlb  32242  nmlnop0iALT  32313  nmopun  32332  nmcexi  32344  branmfn  32423  pjnmopi  32466  fpwrelmapffslem  33043  ldlfcntref  34210  esumc  34407  orvcval2  34815  derangenlem  35617  satfrnmapom  35816  fmlaomn0  35836  fmlasucdisj  35845  dmopab3rexdif  35851  2goelgoanfmla1  35870  mclsssvlem  36008  mclsind  36016  dfon2lem3  36229  dfon2lem7  36233  fnimage  36373  imageval  36374  dfttc4  36985  poimirlem4  38219  poimirlem5  38220  poimirlem6  38221  poimirlem7  38222  poimirlem8  38223  poimirlem9  38224  poimirlem10  38225  poimirlem11  38226  poimirlem12  38227  poimirlem13  38228  poimirlem14  38229  poimirlem15  38230  poimirlem16  38231  poimirlem17  38232  poimirlem18  38233  poimirlem19  38234  poimirlem20  38235  poimirlem21  38236  poimirlem22  38237  poimirlem25  38240  poimirlem26  38241  poimirlem27  38242  poimirlem29  38244  poimirlem31  38246  mblfinlem3  38254  mblfinlem4  38255  ismblfin  38256  itg2addnc  38269  sdclem2  38337  sdclem1  38338  heibor1lem  38404  glbconxN  40098  pmapglbx  40489  dvhb1dimN  41706  sticksstones10  42868  sticksstones11  42869  sticksstones12a  42870  sticksstones12  42871  sticksstones17  42876  sticksstones18  42877  sticksstones19  42878  redvmptabs  43067  abbibw  43357  eldiophss  43453  setindtrs  43700  hbtlem2  43799  hbtlem5  43803  rngunsnply  43844  oaun3lem1  44049  oadif1lem  44054  oadif1  44055  dftrcl3  44394  brtrclfv2  44401  dfrtrcl3  44407  dfhe3  44449  cpcolld  44916  nzss  44975  upbdrech  45972  fourierdlem36  46805  sge0resplit  47068  hoidmvlelem1  47257  fsetsniunop  47731  elsprel  48169  ixpv  49613  iinfconstbas  49789  setrec2lem1  50416