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

Theorem elabg 3339
 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 3336 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 3192 This theorem is referenced by:  elab2g  3341  intmin3  4477  elxpi  5100  finds  7054  wfrlem15  7389  elfi  8279  inficl  8291  dffi3  8297  scott0  8709  elgch  9404  nqpr  9796  hashf1lem1  13193  cshword  13490  trclublem  13684  cotrtrclfv  13703  dfiso2  16372  lubval  16924  glbval  16937  efgcpbllemb  18108  frgpuplem  18125  lspsn  18942  mpfind  19476  pf1ind  19659  eltg  20701  eltg2  20702  islocfin  21260  fbssfi  21581  isewlk  26402  elabreximd  29236  abfmpunirn  29335  orvcval  30342  nosifv  31629  nosires  31630  poimirlem3  33083  poimirlem25  33105  islshpkrN  33926  setindtrs  37111  rngunsnply  37263  frege55lem1c  37731  nzss  38037  elabrexg  38728  ismea  40005  afvelrnb  40577  afvelrnb0  40578  cshword2  40766
 Copyright terms: Public domain W3C validator