Theorem 2sb5rf 2451

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 2103	. . . 4 |- ( E. w ( ( z = x /\ w = y ) /\ ph ) <-> ( E. w ( z = x /\ w = y ) /\ ph ) )
3	2	exbii 1774	. . 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 2103	. . 3 |- ( E. z ( E. w ( z = x /\ w = y ) /\ ph ) <-> ( E. z E. w ( z = x /\ w = y ) /\ ph ) )
6	3, 5	bitri 264	. 2 |- ( E. z E. w ( ( z = x /\ w = y ) /\ ph ) <-> ( E. z E. w ( z = x /\ w = y ) /\ ph ) )
7		sbequ12r 2112	. . . . 5 |- ( z = x -> ( [ z / x ] [ w / y ] ph <-> [ w / y ] ph ) )
8		sbequ12r 2112	. . . . 5 |- ( w = y -> ( [ w / y ] ph <-> ph ) )
9	7, 8	sylan9bb 736	. . . 4 |- ( ( z = x /\ w = y ) -> ( [ z / x ] [ w / y ] ph <-> ph ) )
10	9	pm5.32i 669	. . 3 |- ( ( ( z = x /\ w = y ) /\ [ z / x ] [ w / y ] ph ) <-> ( ( z = x /\ w = y ) /\ ph ) )
11	10	2exbii 1775	. 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 2450	. . 3 |- E. z E. w ( z = x /\ w = y )
13	12	biantrur 527	. 2 |- ( ph <-> ( E. z E. w ( z = x /\ w = y ) /\ ph ) )
14	6, 11, 13	3bitr4ri 293	1 |- ( ph <-> E. z E. w ( ( z = x /\ w = y ) /\ [ z / x ] [ w / y ] ph ) )

Syntax hints:   <-> wb 196   /\ wa 384   E.wex 1704   F/wnf 1708   [wsb 1880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881

This theorem is referenced by:  sbel2x  2459