Theorem clelsb3 2942

Description: Substitution applied to an atomic wff (class version of elsb3 2122). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)

Assertion

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

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝐴(𝑦)

Proof of Theorem clelsb3

Dummy variable 𝑤 is distinct from all other variables.

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

Syntax hints:   ↔ wb 208  [wsb 2069   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clel 2895

This theorem is referenced by:  hblem  2945  hblemg  2946  abbi2dv  2952  nfcrii  2972  clelsb3fw  2983  clelsb3f  2984  cbvreuw  3445  cbvreu  3449  sbcel1v  3841  sbcel1vOLD  3842  rmo3  3874  rmo3OLD  3875  kmlem15  9592  iuninc  30314  measiuns  31478  ballotlemodife  31757  bj-nfcf  34244  wl-dfrabv  34864  wl-clelsb3df  34865  wl-dfrabf  34866  ellimcabssub0  41905