Metamath Proof Explorer

Theorem nfra2w

Description: Similar to Lemma 24 of Monk2 p. 114, except the quantification of the antecedent is restricted. Derived automatically from hbra2VD . Version of nfra2 with a disjoint variable condition, which does not require ax-13 . (Contributed by Alan Sare, 31-Dec-2011) (Revised by Gino Giotto, 24-Sep-2024)

Ref Expression
Assertion nfra2w ⊢ Ⅎ 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 φ