Theorem elfvmptrab1

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. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker elfvmptrab1w when possible. (Contributed by Alexander van der Vekens, 15-Jul-2018) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		elfvmptrab1.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ { 𝑦 ∈ ⦋ 𝑥 / 𝑚 ⦌ 𝑀 ∣ 𝜑 } )
2		elfvmptrab1.v	⊢ ( 𝑋 ∈ 𝑉 → ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∈ V )
3		ne0i	⊢ ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) → ( 𝐹 ‘ 𝑋 ) ≠ ∅ )
4		ndmfv	⊢ ( ¬ 𝑋 ∈ dom 𝐹 → ( 𝐹 ‘ 𝑋 ) = ∅ )
5	4	necon1ai	⊢ ( ( 𝐹 ‘ 𝑋 ) ≠ ∅ → 𝑋 ∈ dom 𝐹 )
6	1	dmmptss	⊢ dom 𝐹 ⊆ 𝑉
7	6	sseli	⊢ ( 𝑋 ∈ dom 𝐹 → 𝑋 ∈ 𝑉 )
8		rabexg	⊢ ( ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∈ V → { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } ∈ V )
9	7 2 8	3syl	⊢ ( 𝑋 ∈ dom 𝐹 → { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } ∈ V )
10		nfcv	⊢ Ⅎ 𝑥 𝑋
11		nfsbc1v	⊢ Ⅎ 𝑥 [ 𝑋 / 𝑥 ] 𝜑
12		nfcv	⊢ Ⅎ 𝑥 𝑀
13	10 12	nfcsb	⊢ Ⅎ 𝑥 ⦋ 𝑋 / 𝑚 ⦌ 𝑀
14	11 13	nfrab	⊢ Ⅎ 𝑥 { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 }
15		csbeq1	⊢ ( 𝑥 = 𝑋 → ⦋ 𝑥 / 𝑚 ⦌ 𝑀 = ⦋ 𝑋 / 𝑚 ⦌ 𝑀 )
16		sbceq1a	⊢ ( 𝑥 = 𝑋 → ( 𝜑 ↔ [ 𝑋 / 𝑥 ] 𝜑 ) )
17	15 16	rabeqbidv	⊢ ( 𝑥 = 𝑋 → { 𝑦 ∈ ⦋ 𝑥 / 𝑚 ⦌ 𝑀 ∣ 𝜑 } = { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } )
18	10 14 17 1	fvmptf	⊢ ( ( 𝑋 ∈ 𝑉 ∧ { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } ∈ V ) → ( 𝐹 ‘ 𝑋 ) = { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } )
19	7 9 18	syl2anc	⊢ ( 𝑋 ∈ dom 𝐹 → ( 𝐹 ‘ 𝑋 ) = { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } )
20	19	eleq2d	⊢ ( 𝑋 ∈ dom 𝐹 → ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) ↔ 𝑌 ∈ { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } ) )
21		elrabi	⊢ ( 𝑌 ∈ { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } → 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 )
22	7 21	anim12i	⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ 𝑌 ∈ { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) )
23	22	ex	⊢ ( 𝑋 ∈ dom 𝐹 → ( 𝑌 ∈ { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) ) )
24	20 23	sylbid	⊢ ( 𝑋 ∈ dom 𝐹 → ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) ) )
25	3 5 24	3syl	⊢ ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) → ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) ) )
26	25	pm2.43i	⊢ ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) )