Metamath Proof Explorer

Theorem nfra2wOLD

Description: Obsolete version of nfra2w as of 31-Oct-2024. (Contributed by Alan Sare, 31-Dec-2011) (Revised by Gino Giotto, 24-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion nfra2wOLD ⊢ Ⅎ y ∀ x ∈ A ∀ y ∈ B φ

Proof

Step Hyp Ref Expression
1 df-ral ⊢ ∀ x ∈ A ∀ y ∈ B φ ↔ ∀ x x ∈ A → ∀ y ∈ B φ
2 df-ral ⊢ ∀ y ∈ B φ ↔ ∀ y y ∈ B → φ
3 2 imbi2i ⊢ x ∈ A → ∀ y ∈ B φ ↔ x ∈ A → ∀ y y ∈ B → φ
4 3 albii ⊢ ∀ x x ∈ A → ∀ y ∈ B φ ↔ ∀ x x ∈ A → ∀ y y ∈ B → φ
5 1 4 bitri ⊢ ∀ x ∈ A ∀ y ∈ B φ ↔ ∀ x x ∈ A → ∀ y y ∈ B → φ
6 nfa1 ⊢ Ⅎ y ∀ y ∀ x x ∈ A → y ∈ B → φ
7 alcom ⊢ ∀ y ∀ x x ∈ A → y ∈ B → φ ↔ ∀ x ∀ y x ∈ A → y ∈ B → φ
8 19.21v ⊢ ∀ y x ∈ A → y ∈ B → φ ↔ x ∈ A → ∀ y y ∈ B → φ
9 8 albii ⊢ ∀ x ∀ y x ∈ A → y ∈ B → φ ↔ ∀ x x ∈ A → ∀ y y ∈ B → φ
10 7 9 bitri ⊢ ∀ y ∀ x x ∈ A → y ∈ B → φ ↔ ∀ x x ∈ A → ∀ y y ∈ B → φ
11 10 nfbii ⊢ Ⅎ y ∀ y ∀ x x ∈ A → y ∈ B → φ ↔ Ⅎ y ∀ x x ∈ A → ∀ y y ∈ B → φ
12 6 11 mpbi ⊢ Ⅎ y ∀ x x ∈ A → ∀ y y ∈ B → φ
13 5 12 nfxfr ⊢ Ⅎ y ∀ x ∈ A ∀ y ∈ B φ