Theorem clelsb3 2940

Description: Substitution applied to an atomic wff (class version of elsb3 2118). (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 2895	. 2 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))
2		eleq1w 2895	. 2 ⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
3	1, 2	sbievw2 2103	1 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)

Syntax hints:   ↔ wb 208  [wsb 2065   ∈ wcel 2110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066  df-clel 2893

This theorem is referenced by:  hblem  2943  hblemg  2944  abbi2dv  2950  nfcrii  2970  clelsb3fw  2981  clelsb3f  2982  cbvreuw  3443  cbvreu  3447  sbcel1v  3838  sbcel1vOLD  3839  rmo3  3871  rmo3OLD  3872  kmlem15  9584  iuninc  30306  measiuns  31471  ballotlemodife  31750  bj-nfcf  34237  wl-dfrabv  34856  wl-clelsb3df  34857  wl-dfrabf  34858  ellimcabssub0  41891