Metamath Proof Explorer

Theorem hbra2VD

Description: Virtual deduction proof of nfra2 . 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. B A. x e. A ph -> A. y A. y e. B A. x e. A ph )
2::	\|- ( A. x e. A A. y e. B ph <-> A. y e. B A. x e. A ph )
3:1,2,?: e00	\|- ( A. x e. A A. y e. B ph -> A. y A. y e. B A. x e. A ph )
4:2:	\|- A. y ( A. x e. A A. y e. B ph <-> A. y e. B A. x e. A ph )
5:4,?: e0a	\|- ( A. y A. x e. A A. y e. B ph <-> A. y A. y e. B A. x e. A ph )
qed:3,5,?: e00	\|- ( A. x e. A A. y e. B ph -> A. y A. x e. A A. y e. B ph )

(Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	hbra2VD	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 → ∀ 𝑦 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		ralcom	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 𝜑 )
2		hbra1	⊢ ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 𝜑 → ∀ 𝑦 ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 𝜑 )
3	1 2	hbxfrbi	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 → ∀ 𝑦 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 )