Theorem clelsb3f 28109

Description: Substitution applied to an atomic wff (class version of elsb3 2262). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (Revised by Thierry Arnoux, 13-Mar-2017.)

Hypothesis

Ref	Expression
clelsb3f.1	|- F/_ y A

Assertion

Ref	Expression
clelsb3f	|- ( [ x / y ] y e. A <-> x e. A )

Proof of Theorem clelsb3f

Dummy variable w is distinct from all other variables.

Step	Hyp	Ref	Expression
1		clelsb3f.1	. . . 4 |- F/_ y A
2	1	nfcri 2585	. . 3 |- F/ y w e. A
3	2	sbco2 2243	. 2 |- ( [ x / y ] [ y / w ] w e. A <-> [ x / w ] w e. A )
4		nfv 1760	. . . 4 |- F/ w y e. A
5		eleq1 2516	. . . 4 |- ( w = y -> ( w e. A <-> y e. A ) )
6	4, 5	sbie 2236	. . 3 |- ( [ y / w ] w e. A <-> y e. A )
7	6	sbbii 1803	. 2 |- ( [ x / y ] [ y / w ] w e. A <-> [ x / y ] y e. A )
8		nfv 1760	. . 3 |- F/ w x e. A
9		eleq1 2516	. . 3 |- ( w = x -> ( w e. A <-> x e. A ) )
10	8, 9	sbie 2236	. 2 |- ( [ x / w ] w e. A <-> x e. A )
11	3, 7, 10	3bitr3i 279	1 |- ( [ x / y ] y e. A <-> x e. A )

Syntax hints:   <-> wb 188   [wsb 1796   e. wcel 1886   F/_wnfc 2578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-ex 1663  df-nf 1667  df-sb 1797  df-cleq 2443  df-clel 2446  df-nfc 2580

This theorem is referenced by:  rmo3f  28124  suppss2fOLD  28230  suppss2f  28231  fmptdF  28248  disjdsct  28276  esumpfinvalf  28890