Theorem 2sb5rf 2290

Description: Reversed double substitution. (Contributed by NM, 3-Feb-2005.) (Revised by Mario Carneiro, 6-Oct-2016.) Remove distinct variable constraints. (Revised by Wolf Lammen, 28-Sep-2018.)

Hypotheses

Ref	Expression
2sb5rf.1	|- F/ z ph
2sb5rf.2	|- F/ w ph

Assertion

Ref	Expression
2sb5rf	|- ( ph <-> E. z E. w ( ( z = x /\ w = y ) /\ [ z / x ] [ w / y ] ph ) )

Distinct variable group:   z, w

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

Proof of Theorem 2sb5rf

Step	Hyp	Ref	Expression
1		2sb5rf.2	. . . . 5 |- F/ w ph
2	1	19.41 2061	. . . 4 |- ( E. w ( ( z = x /\ w = y ) /\ ph ) <-> ( E. w ( z = x /\ w = y ) /\ ph ) )
3	2	exbii 1728	. . 3 |- ( E. z E. w ( ( z = x /\ w = y ) /\ ph ) <-> E. z ( E. w ( z = x /\ w = y ) /\ ph ) )
4		2sb5rf.1	. . . 4 |- F/ z ph
5	4	19.41 2061	. . 3 |- ( E. z ( E. w ( z = x /\ w = y ) /\ ph ) <-> ( E. z E. w ( z = x /\ w = y ) /\ ph ) )
6	3, 5	bitri 257	. 2 |- ( E. z E. w ( ( z = x /\ w = y ) /\ ph ) <-> ( E. z E. w ( z = x /\ w = y ) /\ ph ) )
7		sbequ12r 2094	. . . . 5 |- ( z = x -> ( [ z / x ] [ w / y ] ph <-> [ w / y ] ph ) )
8		sbequ12r 2094	. . . . 5 |- ( w = y -> ( [ w / y ] ph <-> ph ) )
9	7, 8	sylan9bb 711	. . . 4 |- ( ( z = x /\ w = y ) -> ( [ z / x ] [ w / y ] ph <-> ph ) )
10	9	pm5.32i 647	. . 3 |- ( ( ( z = x /\ w = y ) /\ [ z / x ] [ w / y ] ph ) <-> ( ( z = x /\ w = y ) /\ ph ) )
11	10	2exbii 1729	. 2 |- ( E. z E. w ( ( z = x /\ w = y ) /\ [ z / x ] [ w / y ] ph ) <-> E. z E. w ( ( z = x /\ w = y ) /\ ph ) )
12		2ax6e 2289	. . 3 |- E. z E. w ( z = x /\ w = y )
13	12	biantrur 513	. 2 |- ( ph <-> ( E. z E. w ( z = x /\ w = y ) /\ ph ) )
14	6, 11, 13	3bitr4ri 286	1 |- ( ph <-> E. z E. w ( ( z = x /\ w = y ) /\ [ z / x ] [ w / y ] ph ) )

Syntax hints:   <-> wb 189   /\ wa 375   E.wex 1673   F/wnf 1677   [wsb 1807

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101

This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1674  df-nf 1678  df-sb 1808

This theorem is referenced by:  sbel2x  2298