Theorem sbabel 2516

Description: Theorem to move a substitution in and out of a class abstraction. (Contributed by NM, 27-Sep-2003.) (Revised by Mario Carneiro, 7-Oct-2016.)

Hypothesis

Ref	Expression
sbabel.1	|- F/_xA

Assertion

Ref	Expression
sbabel	|- ([y / x]{z | ph} e. A <-> {z | [y / x]ph} e. A)

Distinct variable groups:   x,z   y,z

Allowed substitution hints:   ph(x,y,z)   A(x,y,z)

Proof of Theorem sbabel

Dummy variable v is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sbex 2128	. . 3 |- ([y / x]E.v(v = {z | ph} /\ v e. A) <-> E.v[y / x](v = {z | ph} /\ v e. A))
2		sban 2069	. . . . 5 |- ([y / x](v = {z | ph} /\ v e. A) <-> ([y / x]v = {z | ph} /\ [y / x]v e. A))
3		nfv 1619	. . . . . . . . . 10 |- F/x z e. v
4	3	sbf 2026	. . . . . . . . 9 |- ([y / x]z e. v <-> z e. v)
5	4	sbrbis 2073	. . . . . . . 8 |- ([y / x](z e. v <-> ph) <-> (z e. v <-> [y / x]ph))
6	5	sbalv 2129	. . . . . . 7 |- ([y / x]A.z(z e. v <-> ph) <-> A.z(z e. v <-> [y / x]ph))
7		abeq2 2459	. . . . . . . 8 |- (v = {z | ph} <-> A.z(z e. v <-> ph))
8	7	sbbii 1653	. . . . . . 7 |- ([y / x]v = {z | ph} <-> [y / x]A.z(z e. v <-> ph))
9		abeq2 2459	. . . . . . 7 |- (v = {z | [y / x]ph} <-> A.z(z e. v <-> [y / x]ph))
10	6, 8, 9	3bitr4i 268	. . . . . 6 |- ([y / x]v = {z | ph} <-> v = {z | [y / x]ph})
11		sbabel.1	. . . . . . . 8 |- F/_xA
12	11	nfcri 2484	. . . . . . 7 |- F/x v e. A
13	12	sbf 2026	. . . . . 6 |- ([y / x]v e. A <-> v e. A)
14	10, 13	anbi12i 678	. . . . 5 |- (([y / x]v = {z | ph} /\ [y / x]v e. A) <-> (v = {z | [y / x]ph} /\ v e. A))
15	2, 14	bitri 240	. . . 4 |- ([y / x](v = {z | ph} /\ v e. A) <-> (v = {z | [y / x]ph} /\ v e. A))
16	15	exbii 1582	. . 3 |- (E.v[y / x](v = {z | ph} /\ v e. A) <-> E.v(v = {z | [y / x]ph} /\ v e. A))
17	1, 16	bitri 240	. 2 |- ([y / x]E.v(v = {z | ph} /\ v e. A) <-> E.v(v = {z | [y / x]ph} /\ v e. A))
18		df-clel 2349	. . 3 |- ({z | ph} e. A <-> E.v(v = {z | ph} /\ v e. A))
19	18	sbbii 1653	. 2 |- ([y / x]{z | ph} e. A <-> [y / x]E.v(v = {z | ph} /\ v e. A))
20		df-clel 2349	. 2 |- ({z | [y / x]ph} e. A <-> E.v(v = {z | [y / x]ph} /\ v e. A))
21	17, 19, 20	3bitr4i 268	1 |- ([y / x]{z | ph} e. A <-> {z | [y / x]ph} e. A)

Syntax hints:   <-> wb 176   /\ wa 358  A.wal 1540  E.wex 1541   = wceq 1642  [wsb 1648   e. wcel 1710  {cab 2339   F/_wnfc 2477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479

This theorem is referenced by: (None)