Theorem hbra2VD 16684

Description: Virtual deduction proof of hbra2 2148. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	|- (A.y e. BA.x e. Aph -> A.yA.y e. BA.x e. Aph)
2::	|- (A.x e. AA.y e. Bph <-> A.y e. BA.x e. Aph)
3:1,2,?: e00 16635	|- (A.x e. AA.y e. Bph -> A.yA.y e. BA.x e. Aph)
4:2:	|- A.y(A.x e. AA.y e. Bph <-> A.y e. BA.x e. Aph)
5:4,?: e0_ 16637	|- (A.yA.x e. AA.y e. Bph <-> A.yA.y e. BA.x e. Aph)
qed:3,5,?: e00 16635	|- (A.x e. AA.y e. Bph -> A.yA.x e. AA.y e. Bph)

Assertion

Ref	Expression
hbra2VD	|- (A.x e. A A.y e. B ph -> A.yA.x e. A A.y e. B ph)

Distinct variable groups:   y,A   x,B   x,y

Proof of Theorem hbra2VD

Step	Hyp	Ref	Expression
1		hbra1 2147	. . 3 |- (A.y e. B A.x e. A ph -> A.yA.y e. B A.x e. A ph)
2		ralcom 2242	. . 3 |- (A.x e. A A.y e. B ph <-> A.y e. B A.x e. A ph)
3		imbi1 685	. . . 4 |- ((A.x e. A A.y e. B ph <-> A.y e. B A.x e. A ph) -> ((A.x e. A A.y e. B ph -> A.yA.y e. B A.x e. A ph) <-> (A.y e. B A.x e. A ph -> A.yA.y e. B A.x e. A ph)))
4	3	biimprcd 173	. . 3 |- ((A.y e. B A.x e. A ph -> A.yA.y e. B A.x e. A ph) -> ((A.x e. A A.y e. B ph <-> A.y e. B A.x e. A ph) -> (A.x e. A A.y e. B ph -> A.yA.y e. B A.x e. A ph)))
5	1, 2, 4	e00 16635	. 2 |- (A.x e. A A.y e. B ph -> A.yA.y e. B A.x e. A ph)
6	2	ax-gen 1305	. . 3 |- A.y(A.x e. A A.y e. B ph <-> A.y e. B A.x e. A ph)
7		albi 1344	. . 3 |- (A.y(A.x e. A A.y e. B ph <-> A.y e. B A.x e. A ph) -> (A.yA.x e. A A.y e. B ph <-> A.yA.y e. B A.x e. A ph))
8	6, 7	e0_ 16637	. 2 |- (A.yA.x e. A A.y e. B ph <-> A.yA.y e. B A.x e. A ph)
9		imbi2 686	. . 3 |- ((A.yA.x e. A A.y e. B ph <-> A.yA.y e. B A.x e. A ph) -> ((A.x e. A A.y e. B ph -> A.yA.x e. A A.y e. B ph) <-> (A.x e. A A.y e. B ph -> A.yA.y e. B A.x e. A ph)))
10	9	biimprcd 173	. 2 |- ((A.x e. A A.y e. B ph -> A.yA.y e. B A.x e. A ph) -> ((A.yA.x e. A A.y e. B ph <-> A.yA.y e. B A.x e. A ph) -> (A.x e. A A.y e. B ph -> A.yA.x e. A A.y e. B ph)))
11	5, 8, 10	e00 16635	1 |- (A.x e. A A.y e. B ph -> A.yA.x e. A A.y e. B ph)

Syntax hints:   -> wi 3   <-> wb 163  A.wal 1296  A.wral 2105

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324

This theorem depends on definitions:  df-bi 164  df-an 242  df-ral 2109

Copyright terms: Public domain