Metamath Proof Explorer


Theorem abfmpeld

Description: Membership in an element of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 19-Oct-2016)

Ref Expression
Hypotheses abfmpeld.1 𝐹 = ( 𝑥𝑉 ↦ { 𝑦𝜓 } )
abfmpeld.2 ( 𝜑 → { 𝑦𝜓 } ∈ V )
abfmpeld.3 ( 𝜑 → ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( 𝜓𝜒 ) ) )
Assertion abfmpeld ( 𝜑 → ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐵 ∈ ( 𝐹𝐴 ) ↔ 𝜒 ) ) )

Proof

Step Hyp Ref Expression
1 abfmpeld.1 𝐹 = ( 𝑥𝑉 ↦ { 𝑦𝜓 } )
2 abfmpeld.2 ( 𝜑 → { 𝑦𝜓 } ∈ V )
3 abfmpeld.3 ( 𝜑 → ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( 𝜓𝜒 ) ) )
4 2 alrimiv ( 𝜑 → ∀ 𝑥 { 𝑦𝜓 } ∈ V )
5 csbexg ( ∀ 𝑥 { 𝑦𝜓 } ∈ V → 𝐴 / 𝑥 { 𝑦𝜓 } ∈ V )
6 4 5 syl ( 𝜑 𝐴 / 𝑥 { 𝑦𝜓 } ∈ V )
7 1 fvmpts ( ( 𝐴𝑉 𝐴 / 𝑥 { 𝑦𝜓 } ∈ V ) → ( 𝐹𝐴 ) = 𝐴 / 𝑥 { 𝑦𝜓 } )
8 6 7 sylan2 ( ( 𝐴𝑉𝜑 ) → ( 𝐹𝐴 ) = 𝐴 / 𝑥 { 𝑦𝜓 } )
9 csbab 𝐴 / 𝑥 { 𝑦𝜓 } = { 𝑦[ 𝐴 / 𝑥 ] 𝜓 }
10 8 9 eqtrdi ( ( 𝐴𝑉𝜑 ) → ( 𝐹𝐴 ) = { 𝑦[ 𝐴 / 𝑥 ] 𝜓 } )
11 10 eleq2d ( ( 𝐴𝑉𝜑 ) → ( 𝐵 ∈ ( 𝐹𝐴 ) ↔ 𝐵 ∈ { 𝑦[ 𝐴 / 𝑥 ] 𝜓 } ) )
12 11 adantl ( ( 𝐵𝑊 ∧ ( 𝐴𝑉𝜑 ) ) → ( 𝐵 ∈ ( 𝐹𝐴 ) ↔ 𝐵 ∈ { 𝑦[ 𝐴 / 𝑥 ] 𝜓 } ) )
13 simpll ( ( ( 𝐴𝑉𝜑 ) ∧ 𝑦 = 𝐵 ) → 𝐴𝑉 )
14 3 ancomsd ( 𝜑 → ( ( 𝑦 = 𝐵𝑥 = 𝐴 ) → ( 𝜓𝜒 ) ) )
15 14 adantl ( ( 𝐴𝑉𝜑 ) → ( ( 𝑦 = 𝐵𝑥 = 𝐴 ) → ( 𝜓𝜒 ) ) )
16 15 impl ( ( ( ( 𝐴𝑉𝜑 ) ∧ 𝑦 = 𝐵 ) ∧ 𝑥 = 𝐴 ) → ( 𝜓𝜒 ) )
17 13 16 sbcied ( ( ( 𝐴𝑉𝜑 ) ∧ 𝑦 = 𝐵 ) → ( [ 𝐴 / 𝑥 ] 𝜓𝜒 ) )
18 17 ex ( ( 𝐴𝑉𝜑 ) → ( 𝑦 = 𝐵 → ( [ 𝐴 / 𝑥 ] 𝜓𝜒 ) ) )
19 18 alrimiv ( ( 𝐴𝑉𝜑 ) → ∀ 𝑦 ( 𝑦 = 𝐵 → ( [ 𝐴 / 𝑥 ] 𝜓𝜒 ) ) )
20 elabgt ( ( 𝐵𝑊 ∧ ∀ 𝑦 ( 𝑦 = 𝐵 → ( [ 𝐴 / 𝑥 ] 𝜓𝜒 ) ) ) → ( 𝐵 ∈ { 𝑦[ 𝐴 / 𝑥 ] 𝜓 } ↔ 𝜒 ) )
21 19 20 sylan2 ( ( 𝐵𝑊 ∧ ( 𝐴𝑉𝜑 ) ) → ( 𝐵 ∈ { 𝑦[ 𝐴 / 𝑥 ] 𝜓 } ↔ 𝜒 ) )
22 12 21 bitrd ( ( 𝐵𝑊 ∧ ( 𝐴𝑉𝜑 ) ) → ( 𝐵 ∈ ( 𝐹𝐴 ) ↔ 𝜒 ) )
23 22 an13s ( ( 𝜑 ∧ ( 𝐴𝑉𝐵𝑊 ) ) → ( 𝐵 ∈ ( 𝐹𝐴 ) ↔ 𝜒 ) )
24 23 ex ( 𝜑 → ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐵 ∈ ( 𝐹𝐴 ) ↔ 𝜒 ) ) )