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

Theorem elabg 3209
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 2646 . 2 𝑥𝐴
2 nfv 1792 . 2 𝑥𝜓
3 elabg.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
41, 2, 3elabgf 3206 1 (𝐴𝑉 → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 191   = wceq 1468  wcel 1937  {cab 2491
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485
This theorem depends on definitions:  df-bi 192  df-an 380  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-v 3068
This theorem is referenced by:  elab2g  3211  intmin3  4292  elxpi  4896  finds  6796  wfrlem15  7127  elfi  8012  inficl  8024  dffi3  8030  scott0  8442  elgch  9132  nqpr  9524  hashf1lem1  12741  cshword  13026  trclublem  13217  cotrtrclfv  13236  dfiso2  15843  lubval  16395  glbval  16408  efgcpbllemb  17566  frgpuplem  17583  lspsn  18385  mpfind  18918  pf1ind  19101  eltg  20130  eltg2  20131  islocfin  20689  fbssfi  21010  elabreximd  28305  abfmpunirn  28409  orvcval  29444  poimirlem3  32181  poimirlem25  32203  islshpkrN  32926  setindtrs  36120  rngunsnply  36279  frege55lem1c  36751  nzss  37023  elabrexg  37716  ismea  38739  isome  38779  afvelrnb  39185  afvelrnb0  39186  cshword2  39500  isewlk  40204
  Copyright terms: Public domain W3C validator