Proof of Theorem abfmpeld
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | abfmpeld.2 | . . . . . . . . . 10
⊢ (𝜑 → {𝑦 ∣ 𝜓} ∈ V) | 
| 2 | 1 | alrimiv 1926 | . . . . . . . . 9
⊢ (𝜑 → ∀𝑥{𝑦 ∣ 𝜓} ∈ V) | 
| 3 |  | csbexg 5309 | . . . . . . . . 9
⊢
(∀𝑥{𝑦 ∣ 𝜓} ∈ V → ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜓} ∈ V) | 
| 4 | 2, 3 | syl 17 | . . . . . . . 8
⊢ (𝜑 → ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜓} ∈ V) | 
| 5 |  | abfmpeld.1 | . . . . . . . . 9
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∣ 𝜓}) | 
| 6 | 5 | fvmpts 7018 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜓} ∈ V) → (𝐹‘𝐴) = ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜓}) | 
| 7 | 4, 6 | sylan2 593 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝜑) → (𝐹‘𝐴) = ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜓}) | 
| 8 |  | csbab 4439 | . . . . . . 7
⊢
⦋𝐴 /
𝑥⦌{𝑦 ∣ 𝜓} = {𝑦 ∣ [𝐴 / 𝑥]𝜓} | 
| 9 | 7, 8 | eqtrdi 2792 | . . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝜑) → (𝐹‘𝐴) = {𝑦 ∣ [𝐴 / 𝑥]𝜓}) | 
| 10 | 9 | eleq2d 2826 | . . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝜑) → (𝐵 ∈ (𝐹‘𝐴) ↔ 𝐵 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝜓})) | 
| 11 | 10 | adantl 481 | . . . 4
⊢ ((𝐵 ∈ 𝑊 ∧ (𝐴 ∈ 𝑉 ∧ 𝜑)) → (𝐵 ∈ (𝐹‘𝐴) ↔ 𝐵 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝜓})) | 
| 12 |  | simpll 766 | . . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝜑) ∧ 𝑦 = 𝐵) → 𝐴 ∈ 𝑉) | 
| 13 |  | abfmpeld.3 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜓 ↔ 𝜒))) | 
| 14 | 13 | ancomsd 465 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑦 = 𝐵 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))) | 
| 15 | 14 | adantl 481 | . . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝜑) → ((𝑦 = 𝐵 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))) | 
| 16 | 15 | impl 455 | . . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝜑) ∧ 𝑦 = 𝐵) ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) | 
| 17 | 12, 16 | sbcied 3831 | . . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝜑) ∧ 𝑦 = 𝐵) → ([𝐴 / 𝑥]𝜓 ↔ 𝜒)) | 
| 18 | 17 | ex 412 | . . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝜑) → (𝑦 = 𝐵 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒))) | 
| 19 | 18 | alrimiv 1926 | . . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝜑) → ∀𝑦(𝑦 = 𝐵 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒))) | 
| 20 |  | elabgt 3671 | . . . . 5
⊢ ((𝐵 ∈ 𝑊 ∧ ∀𝑦(𝑦 = 𝐵 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒))) → (𝐵 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝜓} ↔ 𝜒)) | 
| 21 | 19, 20 | sylan2 593 | . . . 4
⊢ ((𝐵 ∈ 𝑊 ∧ (𝐴 ∈ 𝑉 ∧ 𝜑)) → (𝐵 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝜓} ↔ 𝜒)) | 
| 22 | 11, 21 | bitrd 279 | . . 3
⊢ ((𝐵 ∈ 𝑊 ∧ (𝐴 ∈ 𝑉 ∧ 𝜑)) → (𝐵 ∈ (𝐹‘𝐴) ↔ 𝜒)) | 
| 23 | 22 | an13s 651 | . 2
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (𝐵 ∈ (𝐹‘𝐴) ↔ 𝜒)) | 
| 24 | 23 | ex 412 | 1
⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∈ (𝐹‘𝐴) ↔ 𝜒))) |