Metamath Proof Explorer

Theorem nfixp

Description: Bound-variable hypothesis builder for indexed Cartesian product. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfixpw when possible. (Contributed by Mario Carneiro, 15-Oct-2016) (New usage is discouraged.)

Ref Expression
Hypotheses nfixp.1 ⊢ Ⅎ _ y A
nfixp.2 ⊢ Ⅎ _ y B
Assertion nfixp ⊢ Ⅎ _ y ⨉ x ∈ A B

Proof

Step Hyp Ref Expression
1 nfixp.1 ⊢ Ⅎ _ y A
2 nfixp.2 ⊢ Ⅎ _ y B
3 df-ixp ⊢ ⨉ x ∈ A B = z | z Fn x | x ∈ A ∧ ∀ x ∈ A z ⁡ x ∈ B
4 nfcv ⊢ Ⅎ _ y z
5 nftru ⊢ Ⅎ x ⊤
6 nfcvf ⊢ ¬ ∀ y y = x → Ⅎ _ y x
7 6 adantl ⊢ ⊤ ∧ ¬ ∀ y y = x → Ⅎ _ y x
8 1 a1i ⊢ ⊤ ∧ ¬ ∀ y y = x → Ⅎ _ y A
9 7 8 nfeld ⊢ ⊤ ∧ ¬ ∀ y y = x → Ⅎ y x ∈ A
10 5 9 nfabd2 ⊢ ⊤ → Ⅎ _ y x | x ∈ A
11 10 mptru ⊢ Ⅎ _ y x | x ∈ A
12 4 11 nffn ⊢ Ⅎ y z Fn x | x ∈ A
13 df-ral ⊢ ∀ x ∈ A z ⁡ x ∈ B ↔ ∀ x x ∈ A → z ⁡ x ∈ B
14 4 a1i ⊢ ⊤ ∧ ¬ ∀ y y = x → Ⅎ _ y z
15 14 7 nffvd ⊢ ⊤ ∧ ¬ ∀ y y = x → Ⅎ _ y z ⁡ x
16 2 a1i ⊢ ⊤ ∧ ¬ ∀ y y = x → Ⅎ _ y B
17 15 16 nfeld ⊢ ⊤ ∧ ¬ ∀ y y = x → Ⅎ y z ⁡ x ∈ B
18 9 17 nfimd ⊢ ⊤ ∧ ¬ ∀ y y = x → Ⅎ y x ∈ A → z ⁡ x ∈ B
19 5 18 nfald2 ⊢ ⊤ → Ⅎ y ∀ x x ∈ A → z ⁡ x ∈ B
20 19 mptru ⊢ Ⅎ y ∀ x x ∈ A → z ⁡ x ∈ B
21 13 20 nfxfr ⊢ Ⅎ y ∀ x ∈ A z ⁡ x ∈ B
22 12 21 nfan ⊢ Ⅎ y z Fn x | x ∈ A ∧ ∀ x ∈ A z ⁡ x ∈ B
23 22 nfab ⊢ Ⅎ _ y z | z Fn x | x ∈ A ∧ ∀ x ∈ A z ⁡ x ∈ B
24 3 23 nfcxfr ⊢ Ⅎ _ y ⨉ x ∈ A B