Theorem elfvmptrab1w

Description: Implications for the value of a function defined by the maps-to notation with a class abstraction as a result having an element. Here, the base set of the class abstraction depends on the argument of the function. Version of elfvmptrab1 with a disjoint variable condition, which does not require ax-13 . (Contributed by Alexander van der Vekens, 15-Jul-2018) Avoid ax-13 . (Revised by GG, 26-Jan-2024)

	Ref	Expression
Hypotheses	elfvmptrab1w.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ { 𝑦 ∈ ⦋ 𝑥 / 𝑚 ⦌ 𝑀 ∣ 𝜑 } )
	elfvmptrab1w.v	⊢ ( 𝑋 ∈ 𝑉 → ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∈ V )
Assertion	elfvmptrab1w	⊢ ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		elfvmptrab1w.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ { 𝑦 ∈ ⦋ 𝑥 / 𝑚 ⦌ 𝑀 ∣ 𝜑 } )
2		elfvmptrab1w.v	⊢ ( 𝑋 ∈ 𝑉 → ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∈ V )
3		elfvdm	⊢ ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) → 𝑋 ∈ dom 𝐹 )
4	1	dmmptss	⊢ dom 𝐹 ⊆ 𝑉
5	4	sseli	⊢ ( 𝑋 ∈ dom 𝐹 → 𝑋 ∈ 𝑉 )
6		rabexg	⊢ ( ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∈ V → { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } ∈ V )
7	5 2 6	3syl	⊢ ( 𝑋 ∈ dom 𝐹 → { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } ∈ V )
8		nfcv	⊢ Ⅎ 𝑥 𝑋
9		nfsbc1v	⊢ Ⅎ 𝑥 [ 𝑋 / 𝑥 ] 𝜑
10		nfcv	⊢ Ⅎ 𝑥 𝑀
11	8 10	nfcsbw	⊢ Ⅎ 𝑥 ⦋ 𝑋 / 𝑚 ⦌ 𝑀
12	9 11	nfrabw	⊢ Ⅎ 𝑥 { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 }
13		csbeq1	⊢ ( 𝑥 = 𝑋 → ⦋ 𝑥 / 𝑚 ⦌ 𝑀 = ⦋ 𝑋 / 𝑚 ⦌ 𝑀 )
14		sbceq1a	⊢ ( 𝑥 = 𝑋 → ( 𝜑 ↔ [ 𝑋 / 𝑥 ] 𝜑 ) )
15	13 14	rabeqbidv	⊢ ( 𝑥 = 𝑋 → { 𝑦 ∈ ⦋ 𝑥 / 𝑚 ⦌ 𝑀 ∣ 𝜑 } = { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } )
16	8 12 15 1	fvmptf	⊢ ( ( 𝑋 ∈ 𝑉 ∧ { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } ∈ V ) → ( 𝐹 ‘ 𝑋 ) = { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } )
17	5 7 16	syl2anc	⊢ ( 𝑋 ∈ dom 𝐹 → ( 𝐹 ‘ 𝑋 ) = { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } )
18	17	eleq2d	⊢ ( 𝑋 ∈ dom 𝐹 → ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) ↔ 𝑌 ∈ { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } ) )
19		elrabi	⊢ ( 𝑌 ∈ { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } → 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 )
20	5 19	anim12i	⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ 𝑌 ∈ { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) )
21	20	ex	⊢ ( 𝑋 ∈ dom 𝐹 → ( 𝑌 ∈ { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) ) )
22	18 21	sylbid	⊢ ( 𝑋 ∈ dom 𝐹 → ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) ) )
23	3 22	mpcom	⊢ ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) )