MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elabg Structured version   Visualization version   GIF version

Theorem elabg 3224
Description: Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. (Contributed by NM, 14-Apr-1995.)
Hypothesis
Ref Expression
elabg.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
elabg (𝐴𝑉 → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
Distinct variable groups:   𝜓,𝑥   𝑥,𝐴
Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem elabg
StepHypRef Expression
1 nfcv 2655 . 2 𝑥𝐴
2 nfv 1796 . 2 𝑥𝜓
3 elabg.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
41, 2, 3elabgf 3221 1 (𝐴𝑉 → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wcel 1938  {cab 2500
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494
This theorem depends on definitions:  df-bi 195  df-an 384  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-v 3079
This theorem is referenced by:  elab2g  3226  intmin3  4338  elxpi  4948  finds  6859  wfrlem15  7190  elfi  8077  inficl  8089  dffi3  8095  scott0  8507  elgch  9198  nqpr  9590  hashf1lem1  12959  cshword  13245  trclublem  13439  cotrtrclfv  13458  dfiso2  16145  lubval  16697  glbval  16710  efgcpbllemb  17897  frgpuplem  17914  lspsn  18725  mpfind  19259  pf1ind  19442  eltg  20473  eltg2  20474  islocfin  21031  fbssfi  21352  elabreximd  28521  abfmpunirn  28621  orvcval  29654  poimirlem3  32457  poimirlem25  32479  islshpkrN  33300  setindtrs  36485  rngunsnply  36644  frege55lem1c  37112  nzss  37420  elabrexg  38111  ismea  39238  isome  39278  afvelrnb  39787  afvelrnb0  39788  cshword2  40195  isewlk  40896
  Copyright terms: Public domain W3C validator