Theorem nfixpw

Description: Bound-variable hypothesis builder for indexed Cartesian product. Version of nfixp with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 15-Oct-2016) (Revised by Gino Giotto, 26-Jan-2024)

	Ref	Expression
Hypotheses	nfixpw.1	⊢ Ⅎ 𝑦 𝐴
	nfixpw.2	⊢ Ⅎ 𝑦 𝐵
Assertion	nfixpw	⊢ Ⅎ 𝑦 X 𝑥 ∈ 𝐴 𝐵

Proof

Step	Hyp	Ref	Expression
1		nfixpw.1	⊢ Ⅎ 𝑦 𝐴
2		nfixpw.2	⊢ Ⅎ 𝑦 𝐵
3		df-ixp	⊢ X 𝑥 ∈ 𝐴 𝐵 = { 𝑧 ∣ ( 𝑧 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ) }
4		nfcv	⊢ Ⅎ 𝑦 𝑧
5		nfcv	⊢ Ⅎ 𝑦 𝑥
6	5 1	nfel	⊢ Ⅎ 𝑦 𝑥 ∈ 𝐴
7	6	nfab	⊢ Ⅎ 𝑦 { 𝑥 ∣ 𝑥 ∈ 𝐴 }
8	7	a1i	⊢ ( ⊤ → Ⅎ 𝑦 { 𝑥 ∣ 𝑥 ∈ 𝐴 } )
9	8	mptru	⊢ Ⅎ 𝑦 { 𝑥 ∣ 𝑥 ∈ 𝐴 }
10	4 9	nffn	⊢ Ⅎ 𝑦 𝑧 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 }
11		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ) )
12		nftru	⊢ Ⅎ 𝑥 ⊤
13	6	a1i	⊢ ( ⊤ → Ⅎ 𝑦 𝑥 ∈ 𝐴 )
14	4	a1i	⊢ ( ⊤ → Ⅎ 𝑦 𝑧 )
15	5	a1i	⊢ ( ⊤ → Ⅎ 𝑦 𝑥 )
16	14 15	nffvd	⊢ ( ⊤ → Ⅎ 𝑦 ( 𝑧 ‘ 𝑥 ) )
17	2	a1i	⊢ ( ⊤ → Ⅎ 𝑦 𝐵 )
18	16 17	nfeld	⊢ ( ⊤ → Ⅎ 𝑦 ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 )
19	13 18	nfimd	⊢ ( ⊤ → Ⅎ 𝑦 ( 𝑥 ∈ 𝐴 → ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ) )
20	12 19	nfald	⊢ ( ⊤ → Ⅎ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ) )
21	20	mptru	⊢ Ⅎ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 )
22	11 21	nfxfr	⊢ Ⅎ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝑧 ‘ 𝑥 ) ∈ 𝐵
23	10 22	nfan	⊢ Ⅎ 𝑦 ( 𝑧 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 )
24	23	nfab	⊢ Ⅎ 𝑦 { 𝑧 ∣ ( 𝑧 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ) }
25	3 24	nfcxfr	⊢ Ⅎ 𝑦 X 𝑥 ∈ 𝐴 𝐵