Theorem 19.12b

Description: Version of 19.12vv with not-free hypotheses, instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010) (Revised by Mario Carneiro, 11-Dec-2016)

	Ref	Expression
Hypotheses	19.12b.1	|- F/ y ph
	19.12b.2	|- F/ x ps
Assertion	19.12b	|- ( E. x A. y ( ph -> ps ) <-> A. y E. x ( ph -> ps ) )

Proof

Step	Hyp	Ref	Expression
1		19.12b.1	|- F/ y ph
2		19.12b.2	|- F/ x ps
3	1	19.21	|- ( A. y ( ph -> ps ) <-> ( ph -> A. y ps ) )
4	3	exbii	|- ( E. x A. y ( ph -> ps ) <-> E. x ( ph -> A. y ps ) )
5	2	nfal	|- F/ x A. y ps
6	5	19.36	|- ( E. x ( ph -> A. y ps ) <-> ( A. x ph -> A. y ps ) )
7	2	19.36	|- ( E. x ( ph -> ps ) <-> ( A. x ph -> ps ) )
8	7	albii	|- ( A. y E. x ( ph -> ps ) <-> A. y ( A. x ph -> ps ) )
9	1	nfal	|- F/ y A. x ph
10	9	19.21	|- ( A. y ( A. x ph -> ps ) <-> ( A. x ph -> A. y ps ) )
11	8 10	bitr2i	|- ( ( A. x ph -> A. y ps ) <-> A. y E. x ( ph -> ps ) )
12	4 6 11	3bitri	|- ( E. x A. y ( ph -> ps ) <-> A. y E. x ( ph -> ps ) )