Metamath Proof Explorer

Theorem ralxpf

Description: Version of ralxp with bound-variable hypotheses. (Contributed by NM, 18-Aug-2006) (Revised by Mario Carneiro, 15-Oct-2016)

Ref Expression
Hypotheses ralxpf.1 ⊢ Ⅎ y φ
ralxpf.2 ⊢ Ⅎ z φ
ralxpf.3 ⊢ Ⅎ x ψ
ralxpf.4 ⊢ x = y z → φ ↔ ψ
Assertion ralxpf ⊢ ∀ x ∈ A × B φ ↔ ∀ y ∈ A ∀ z ∈ B ψ

Proof

Step Hyp Ref Expression
1 ralxpf.1 ⊢ Ⅎ y φ
2 ralxpf.2 ⊢ Ⅎ z φ
3 ralxpf.3 ⊢ Ⅎ x ψ
4 ralxpf.4 ⊢ x = y z → φ ↔ ψ
5 cbvralsvw ⊢ ∀ x ∈ A × B φ ↔ ∀ w ∈ A × B w x φ
6 cbvralsvw ⊢ ∀ z ∈ B u y ψ ↔ ∀ v ∈ B v z u y ψ
7 6 ralbii ⊢ ∀ u ∈ A ∀ z ∈ B u y ψ ↔ ∀ u ∈ A ∀ v ∈ B v z u y ψ
8 nfv ⊢ Ⅎ u ∀ z ∈ B ψ
9 nfcv ⊢ Ⅎ _ y B
10 nfs1v ⊢ Ⅎ y u y ψ
11 9 10 nfralw ⊢ Ⅎ y ∀ z ∈ B u y ψ
12 sbequ12 ⊢ y = u → ψ ↔ u y ψ
13 12 ralbidv ⊢ y = u → ∀ z ∈ B ψ ↔ ∀ z ∈ B u y ψ
14 8 11 13 cbvralw ⊢ ∀ y ∈ A ∀ z ∈ B ψ ↔ ∀ u ∈ A ∀ z ∈ B u y ψ
15 vex ⊢ u ∈ V
16 vex ⊢ v ∈ V
17 15 16 eqvinop ⊢ w = u v ↔ ∃ y ∃ z w = y z ∧ y z = u v
18 1 nfsbv ⊢ Ⅎ y w x φ
19 10 nfsbv ⊢ Ⅎ y v z u y ψ
20 18 19 nfbi ⊢ Ⅎ y w x φ ↔ v z u y ψ
21 2 nfsbv ⊢ Ⅎ z w x φ
22 nfs1v ⊢ Ⅎ z v z u y ψ
23 21 22 nfbi ⊢ Ⅎ z w x φ ↔ v z u y ψ
24 3 4 sbhypf ⊢ w = y z → w x φ ↔ ψ
25 vex ⊢ y ∈ V
26 vex ⊢ z ∈ V
27 25 26 opth ⊢ y z = u v ↔ y = u ∧ z = v
28 sbequ12 ⊢ z = v → u y ψ ↔ v z u y ψ
29 12 28 sylan9bb ⊢ y = u ∧ z = v → ψ ↔ v z u y ψ
30 27 29 sylbi ⊢ y z = u v → ψ ↔ v z u y ψ
31 24 30 sylan9bb ⊢ w = y z ∧ y z = u v → w x φ ↔ v z u y ψ
32 23 31 exlimi ⊢ ∃ z w = y z ∧ y z = u v → w x φ ↔ v z u y ψ
33 20 32 exlimi ⊢ ∃ y ∃ z w = y z ∧ y z = u v → w x φ ↔ v z u y ψ
34 17 33 sylbi ⊢ w = u v → w x φ ↔ v z u y ψ
35 34 ralxp ⊢ ∀ w ∈ A × B w x φ ↔ ∀ u ∈ A ∀ v ∈ B v z u y ψ
36 7 14 35 3bitr4ri ⊢ ∀ w ∈ A × B w x φ ↔ ∀ y ∈ A ∀ z ∈ B ψ
37 5 36 bitri ⊢ ∀ x ∈ A × B φ ↔ ∀ y ∈ A ∀ z ∈ B ψ