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

Theorem elabg 3319
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 2750 . 2 𝑥𝐴
2 nfv 1829 . 2 𝑥𝜓
3 elabg.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
41, 2, 3elabgf 3316 1 (𝐴𝑉 → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wcel 1976  {cab 2595
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174
This theorem is referenced by:  elab2g  3321  intmin3  4434  elxpi  5044  finds  6961  wfrlem15  7293  elfi  8179  inficl  8191  dffi3  8197  scott0  8609  elgch  9300  nqpr  9692  hashf1lem1  13048  cshword  13334  trclublem  13528  cotrtrclfv  13547  dfiso2  16201  lubval  16753  glbval  16766  efgcpbllemb  17937  frgpuplem  17954  lspsn  18769  mpfind  19303  pf1ind  19486  eltg  20514  eltg2  20515  islocfin  21072  fbssfi  21393  elabreximd  28538  abfmpunirn  28638  orvcval  29652  poimirlem3  32385  poimirlem25  32407  islshpkrN  33228  setindtrs  36413  rngunsnply  36565  frege55lem1c  37033  nzss  37341  elabrexg  38032  ismea  39148  isome  39188  afvelrnb  39697  afvelrnb0  39698  cshword2  40105  isewlk  40806
  Copyright terms: Public domain W3C validator