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

Theorem elabg 3503
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 2913 . 2 𝑥𝐴
2 nfv 1995 . 2 𝑥𝜓
3 elabg.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
41, 2, 3elabgf 3500 1 (𝐴𝑉 → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1631  wcel 2145  {cab 2757
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353
This theorem is referenced by:  elab2g  3505  intmin3  4640  elxpi  5271  finds  7240  wfrlem15  7583  elfi  8476  inficl  8488  dffi3  8494  scott0  8914  elgch  9647  nqpr  10039  hashf1lem1  13442  cshword  13747  trclublem  13945  cotrtrclfv  13962  dfiso2  16640  lubval  17193  glbval  17206  efgcpbllemb  18376  frgpuplem  18393  lspsn  19216  mpfind  19752  pf1ind  19935  eltg  20983  eltg2  20984  islocfin  21542  fbssfi  21862  isewlk  26734  elabreximd  29687  abfmpunirn  29793  orvcval  30860  nosupfv  32190  nosupres  32191  nosupbnd1lem3  32194  nosupbnd1lem5  32196  poimirlem3  33746  poimirlem25  33768  islshpkrN  34930  setindtrs  38119  rngunsnply  38270  frege55lem1c  38737  nzss  39043  elabrexg  39729  ismea  41186  afvelrnb  41764  afvelrnb0  41765  cshword2  41966  setis  42973
  Copyright terms: Public domain W3C validator