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

Theorem elabg 3483
 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 2894 . 2 𝑥𝐴
2 nfv 1984 . 2 𝑥𝜓
3 elabg.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
41, 2, 3elabgf 3480 1 (𝐴𝑉 → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   = wceq 1624   ∈ wcel 2131  {cab 2738 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-v 3334 This theorem is referenced by:  elab2g  3485  intmin3  4649  elxpi  5279  finds  7249  wfrlem15  7590  elfi  8476  inficl  8488  dffi3  8494  scott0  8914  elgch  9628  nqpr  10020  hashf1lem1  13423  cshword  13729  trclublem  13927  cotrtrclfv  13944  dfiso2  16625  lubval  17177  glbval  17190  efgcpbllemb  18360  frgpuplem  18377  lspsn  19196  mpfind  19730  pf1ind  19913  eltg  20955  eltg2  20956  islocfin  21514  fbssfi  21834  isewlk  26700  elabreximd  29647  abfmpunirn  29753  orvcval  30820  nosupfv  32150  nosupres  32151  nosupbnd1lem3  32154  nosupbnd1lem5  32156  poimirlem3  33717  poimirlem25  33739  islshpkrN  34902  setindtrs  38086  rngunsnply  38237  frege55lem1c  38704  nzss  39010  elabrexg  39697  ismea  41163  afvelrnb  41741  afvelrnb0  41742  cshword2  41939  setis  42946
 Copyright terms: Public domain W3C validator