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

Theorem elabg 3320
 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 2751 . 2 𝑥𝐴
2 nfv 1830 . 2 𝑥𝜓
3 elabg.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
41, 2, 3elabgf 3317 1 (𝐴𝑉 → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ∈ wcel 1977  {cab 2596 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175 This theorem is referenced by:  elab2g  3322  intmin3  4440  elxpi  5054  finds  6984  wfrlem15  7316  elfi  8202  inficl  8214  dffi3  8220  scott0  8632  elgch  9323  nqpr  9715  hashf1lem1  13096  cshword  13388  trclublem  13582  cotrtrclfv  13601  dfiso2  16255  lubval  16807  glbval  16820  efgcpbllemb  17991  frgpuplem  18008  lspsn  18823  mpfind  19357  pf1ind  19540  eltg  20572  eltg2  20573  islocfin  21130  fbssfi  21451  elabreximd  28732  abfmpunirn  28832  orvcval  29846  poimirlem3  32582  poimirlem25  32604  islshpkrN  33425  setindtrs  36610  rngunsnply  36762  frege55lem1c  37230  nzss  37538  elabrexg  38229  ismea  39344  isome  39384  afvelrnb  39892  afvelrnb0  39893  cshword2  40300  isewlk  40804  setrec1lem1  42233
 Copyright terms: Public domain W3C validator