Theorem 2sb6rf 2452

Description: Reversed double substitution. (Contributed by NM, 3-Feb-2005.) (Revised by Mario Carneiro, 6-Oct-2016.) Remove 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
2sb6rf	|- ( ph <-> A. z A. 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 2sb6rf

Step	Hyp	Ref	Expression
1		sbequ12r 2112	. . . . 5 |- ( z = x -> ( [ z / x ] [ w / y ] ph <-> [ w / y ] ph ) )
2		sbequ12r 2112	. . . . 5 |- ( w = y -> ( [ w / y ] ph <-> ph ) )
3	1, 2	sylan9bb 736	. . . 4 |- ( ( z = x /\ w = y ) -> ( [ z / x ] [ w / y ] ph <-> ph ) )
4	3	pm5.74i 260	. . 3 |- ( ( ( z = x /\ w = y ) -> [ z / x ] [ w / y ] ph ) <-> ( ( z = x /\ w = y ) -> ph ) )
5	4	2albii 1748	. 2 |- ( A. z A. w ( ( z = x /\ w = y ) -> [ z / x ] [ w / y ] ph ) <-> A. z A. w ( ( z = x /\ w = y ) -> ph ) )
6		2sb5rf.2	. . . . 5 |- F/ w ph
7	6	19.23 2080	. . . 4 |- ( A. w ( ( z = x /\ w = y ) -> ph ) <-> ( E. w ( z = x /\ w = y ) -> ph ) )
8	7	albii 1747	. . 3 |- ( A. z A. w ( ( z = x /\ w = y ) -> ph ) <-> A. z ( E. w ( z = x /\ w = y ) -> ph ) )
9		2sb5rf.1	. . . 4 |- F/ z ph
10	9	19.23 2080	. . 3 |- ( A. z ( E. w ( z = x /\ w = y ) -> ph ) <-> ( E. z E. w ( z = x /\ w = y ) -> ph ) )
11	8, 10	bitri 264	. 2 |- ( A. z A. w ( ( 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		pm5.5 351	. . 3 |- ( E. z E. w ( z = x /\ w = y ) -> ( ( E. z E. w ( z = x /\ w = y ) -> ph ) <-> ph ) )
14	12, 13	ax-mp 5	. 2 |- ( ( E. z E. w ( z = x /\ w = y ) -> ph ) <-> ph )
15	5, 11, 14	3bitrri 287	1 |- ( ph <-> A. z A. w ( ( z = x /\ w = y ) -> [ z / x ] [ w / y ] ph ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   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: (None)