Theorem clelsb1 2867

Description: Substitution for the first argument of the membership predicate in an atomic formula (class version of elsb1 2120). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)

Assertion

Ref	Expression
clelsb1	⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝐴(𝑦)

Proof of Theorem clelsb1

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1w 2822	. 2 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))
2		eleq1w 2822	. 2 ⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
3	1, 2	sbievw2 2105	1 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)

Syntax hints:   ↔ wb 209  [wsb 2072   ∈ wcel 2112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-sb 2073  df-clel 2818

This theorem is referenced by:  hblem  2870  hblemg  2871  abbi2dv  2877  nfcriiOLD  2900  clelsb1fw  2911  clelsb1f  2912  cbvreuw  3366  cbvreu  3371  elrabi  3612  sbcel1v  3784  rmo3  3819  kmlem15  9826  iuninc  30776  measiuns  32060  ballotlemodife  32339  bj-nfcf  35013  ellimcabssub0  43021