Proof of Theorem rabeqsnd
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rabeqsnd.3 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝑥 = 𝐵) | 
| 2 | 1 | expl 457 | . . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → 𝑥 = 𝐵)) | 
| 3 | 2 | alrimiv 1927 | . . . 4
⊢ (𝜑 → ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜓) → 𝑥 = 𝐵)) | 
| 4 |  | rabeqsnd.1 | . . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ 𝐴) | 
| 5 |  | rabeqsnd.2 | . . . . . . . 8
⊢ (𝜑 → 𝜒) | 
| 6 | 4, 5 | jca 511 | . . . . . . 7
⊢ (𝜑 → (𝐵 ∈ 𝐴 ∧ 𝜒)) | 
| 7 | 6 | a1d 25 | . . . . . 6
⊢ (𝜑 → (𝑥 = 𝐵 → (𝐵 ∈ 𝐴 ∧ 𝜒))) | 
| 8 | 7 | alrimiv 1927 | . . . . 5
⊢ (𝜑 → ∀𝑥(𝑥 = 𝐵 → (𝐵 ∈ 𝐴 ∧ 𝜒))) | 
| 9 |  | eleq1 2829 | . . . . . . . 8
⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴)) | 
| 10 |  | rabeqsnd.0 | . . . . . . . 8
⊢ (𝑥 = 𝐵 → (𝜓 ↔ 𝜒)) | 
| 11 | 9, 10 | anbi12d 632 | . . . . . . 7
⊢ (𝑥 = 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝐵 ∈ 𝐴 ∧ 𝜒))) | 
| 12 | 11 | pm5.74i 271 | . . . . . 6
⊢ ((𝑥 = 𝐵 → (𝑥 ∈ 𝐴 ∧ 𝜓)) ↔ (𝑥 = 𝐵 → (𝐵 ∈ 𝐴 ∧ 𝜒))) | 
| 13 | 12 | albii 1819 | . . . . 5
⊢
(∀𝑥(𝑥 = 𝐵 → (𝑥 ∈ 𝐴 ∧ 𝜓)) ↔ ∀𝑥(𝑥 = 𝐵 → (𝐵 ∈ 𝐴 ∧ 𝜒))) | 
| 14 | 8, 13 | sylibr 234 | . . . 4
⊢ (𝜑 → ∀𝑥(𝑥 = 𝐵 → (𝑥 ∈ 𝐴 ∧ 𝜓))) | 
| 15 | 3, 14 | jca 511 | . . 3
⊢ (𝜑 → (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜓) → 𝑥 = 𝐵) ∧ ∀𝑥(𝑥 = 𝐵 → (𝑥 ∈ 𝐴 ∧ 𝜓)))) | 
| 16 |  | albiim 1889 | . . 3
⊢
(∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ 𝑥 = 𝐵) ↔ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜓) → 𝑥 = 𝐵) ∧ ∀𝑥(𝑥 = 𝐵 → (𝑥 ∈ 𝐴 ∧ 𝜓)))) | 
| 17 | 15, 16 | sylibr 234 | . 2
⊢ (𝜑 → ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ 𝑥 = 𝐵)) | 
| 18 |  | rabeqsn 4667 | . 2
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜓} = {𝐵} ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ 𝑥 = 𝐵)) | 
| 19 | 17, 18 | sylibr 234 | 1
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝐵}) |