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 ⊢ ∀ x ∈ A ∀ y ∈ B φ → ∀ y ∀ x ∈ A ∀ y ∈ B φ

Proof

Step Hyp Ref Expression
1 ralcom ⊢ ∀ x ∈ A ∀ y ∈ B φ ↔ ∀ y ∈ B ∀ x ∈ A φ
2 hbra1 ⊢ ∀ y ∈ B ∀ x ∈ A φ → ∀ y ∀ y ∈ B ∀ x ∈ A φ
3 1 2 hbxfrbi ⊢ ∀ x ∈ A ∀ y ∈ B φ → ∀ y ∀ x ∈ A ∀ y ∈ B φ