Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  eliminable-velab Structured version   Visualization version   GIF version

Theorem eliminable-velab 34298
Description: A theorem used to prove the base case of the Eliminability Theorem (see section comment): variable belongs to abstraction. (Contributed by BJ, 30-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
eliminable-velab (𝑦 ∈ {𝑥𝜑} ↔ [𝑦 / 𝑥]𝜑)

Proof of Theorem eliminable-velab
StepHypRef Expression
1 df-clab 2780 1 (𝑦 ∈ {𝑥𝜑} ↔ [𝑦 / 𝑥]𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 209  [wsb 2069  wcel 2112  {cab 2779
This theorem depends on definitions:  df-clab 2780
This theorem is referenced by:  eliminable-veqab  34299  eliminable-abeqv  34300  eliminable-abeqab  34301  eliminable-abelab  34303
  Copyright terms: Public domain W3C validator