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

Theorem elabg 3334
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 2761 . 2 𝑥𝐴
2 nfv 1840 . 2 𝑥𝜓
3 elabg.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
41, 2, 3elabgf 3331 1 (𝐴𝑉 → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1480  wcel 1987  {cab 2607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188
This theorem is referenced by:  elab2g  3336  intmin3  4470  elxpi  5090  finds  7039  wfrlem15  7374  elfi  8263  inficl  8275  dffi3  8281  scott0  8693  elgch  9388  nqpr  9780  hashf1lem1  13177  cshword  13474  trclublem  13668  cotrtrclfv  13687  dfiso2  16353  lubval  16905  glbval  16918  efgcpbllemb  18089  frgpuplem  18106  lspsn  18921  mpfind  19455  pf1ind  19638  eltg  20672  eltg2  20673  islocfin  21230  fbssfi  21551  isewlk  26368  elabreximd  29195  abfmpunirn  29294  orvcval  30300  nosifv  31576  nosires  31577  poimirlem3  33044  poimirlem25  33066  islshpkrN  33887  setindtrs  37072  rngunsnply  37224  frege55lem1c  37692  nzss  37998  elabrexg  38689  ismea  39975  afvelrnb  40547  afvelrnb0  40548  cshword2  40736
  Copyright terms: Public domain W3C validator