Metamath Proof Explorer


Theorem isf34lem1

Description: Lemma for isfin3-4 . (Contributed by Stefan O'Rear, 7-Nov-2014)

Ref Expression
Hypothesis compss.a 𝐹 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴𝑥 ) )
Assertion isf34lem1 ( ( 𝐴𝑉𝑋𝐴 ) → ( 𝐹𝑋 ) = ( 𝐴𝑋 ) )

Proof

Step Hyp Ref Expression
1 compss.a 𝐹 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴𝑥 ) )
2 difeq2 ( 𝑥 = 𝑎 → ( 𝐴𝑥 ) = ( 𝐴𝑎 ) )
3 2 cbvmptv ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴𝑥 ) ) = ( 𝑎 ∈ 𝒫 𝐴 ↦ ( 𝐴𝑎 ) )
4 1 3 eqtri 𝐹 = ( 𝑎 ∈ 𝒫 𝐴 ↦ ( 𝐴𝑎 ) )
5 difeq2 ( 𝑎 = 𝑋 → ( 𝐴𝑎 ) = ( 𝐴𝑋 ) )
6 elpw2g ( 𝐴𝑉 → ( 𝑋 ∈ 𝒫 𝐴𝑋𝐴 ) )
7 6 biimpar ( ( 𝐴𝑉𝑋𝐴 ) → 𝑋 ∈ 𝒫 𝐴 )
8 difexg ( 𝐴𝑉 → ( 𝐴𝑋 ) ∈ V )
9 8 adantr ( ( 𝐴𝑉𝑋𝐴 ) → ( 𝐴𝑋 ) ∈ V )
10 4 5 7 9 fvmptd3 ( ( 𝐴𝑉𝑋𝐴 ) → ( 𝐹𝑋 ) = ( 𝐴𝑋 ) )