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 ⊢ F = x ∈ V ⟼ y | ψ
abfmpeld.2 ⊢ φ → y | ψ ∈ V
abfmpeld.3 ⊢ φ → x = A ∧ y = B → ψ ↔ χ
Assertion abfmpeld ⊢ φ → A ∈ V ∧ B ∈ W → B ∈ F ⁡ A ↔ χ

Proof

Step Hyp Ref Expression
1 abfmpeld.1 ⊢ F = x ∈ V ⟼ y | ψ
2 abfmpeld.2 ⊢ φ → y | ψ ∈ V
3 abfmpeld.3 ⊢ φ → x = A ∧ y = B → ψ ↔ χ
4 2 alrimiv ⊢ φ → ∀ x y | ψ ∈ V
5 csbexg ⊢ ∀ x y | ψ ∈ V → ⦋ A / x⦌ y | ψ ∈ V
6 4 5 syl ⊢ φ → ⦋ A / x⦌ y | ψ ∈ V
7 1 fvmpts ⊢ A ∈ V ∧ ⦋ A / x⦌ y | ψ ∈ V → F ⁡ A = ⦋ A / x⦌ y | ψ
8 6 7 sylan2 ⊢ A ∈ V ∧ φ → F ⁡ A = ⦋ A / x⦌ y | ψ
9 csbab ⊢ ⦋ A / x⦌ y | ψ = y | [˙A / x]˙ ψ
10 8 9 eqtrdi ⊢ A ∈ V ∧ φ → F ⁡ A = y | [˙A / x]˙ ψ
11 10 eleq2d ⊢ A ∈ V ∧ φ → B ∈ F ⁡ A ↔ B ∈ y | [˙A / x]˙ ψ
12 11 adantl ⊢ B ∈ W ∧ A ∈ V ∧ φ → B ∈ F ⁡ A ↔ B ∈ y | [˙A / x]˙ ψ
13 simpll ⊢ A ∈ V ∧ φ ∧ y = B → A ∈ V
14 3 ancomsd ⊢ φ → y = B ∧ x = A → ψ ↔ χ
15 14 adantl ⊢ A ∈ V ∧ φ → y = B ∧ x = A → ψ ↔ χ
16 15 impl ⊢ A ∈ V ∧ φ ∧ y = B ∧ x = A → ψ ↔ χ
17 13 16 sbcied ⊢ A ∈ V ∧ φ ∧ y = B → [˙A / x]˙ ψ ↔ χ
18 17 ex ⊢ A ∈ V ∧ φ → y = B → [˙A / x]˙ ψ ↔ χ
19 18 alrimiv ⊢ A ∈ V ∧ φ → ∀ y y = B → [˙A / x]˙ ψ ↔ χ
20 elabgt ⊢ B ∈ W ∧ ∀ y y = B → [˙A / x]˙ ψ ↔ χ → B ∈ y | [˙A / x]˙ ψ ↔ χ
21 19 20 sylan2 ⊢ B ∈ W ∧ A ∈ V ∧ φ → B ∈ y | [˙A / x]˙ ψ ↔ χ
22 12 21 bitrd ⊢ B ∈ W ∧ A ∈ V ∧ φ → B ∈ F ⁡ A ↔ χ
23 22 an13s ⊢ φ ∧ A ∈ V ∧ B ∈ W → B ∈ F ⁡ A ↔ χ
24 23 ex ⊢ φ → A ∈ V ∧ B ∈ W → B ∈ F ⁡ A ↔ χ