Step |
Hyp |
Ref |
Expression |
1 |
|
rabeqsnd.0 |
⊢ ( 𝑥 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) |
2 |
|
rabeqsnd.1 |
⊢ ( 𝜑 → 𝐵 ∈ 𝐴 ) |
3 |
|
rabeqsnd.2 |
⊢ ( 𝜑 → 𝜒 ) |
4 |
|
rabeqsnd.3 |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜓 ) → 𝑥 = 𝐵 ) |
5 |
4
|
expl |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → 𝑥 = 𝐵 ) ) |
6 |
5
|
alrimiv |
⊢ ( 𝜑 → ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → 𝑥 = 𝐵 ) ) |
7 |
2 3
|
jca |
⊢ ( 𝜑 → ( 𝐵 ∈ 𝐴 ∧ 𝜒 ) ) |
8 |
7
|
a1d |
⊢ ( 𝜑 → ( 𝑥 = 𝐵 → ( 𝐵 ∈ 𝐴 ∧ 𝜒 ) ) ) |
9 |
8
|
alrimiv |
⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝐵 → ( 𝐵 ∈ 𝐴 ∧ 𝜒 ) ) ) |
10 |
|
eleq1 |
⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴 ) ) |
11 |
10 1
|
anbi12d |
⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝜒 ) ) ) |
12 |
11
|
pm5.74i |
⊢ ( ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) ↔ ( 𝑥 = 𝐵 → ( 𝐵 ∈ 𝐴 ∧ 𝜒 ) ) ) |
13 |
12
|
albii |
⊢ ( ∀ 𝑥 ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) ↔ ∀ 𝑥 ( 𝑥 = 𝐵 → ( 𝐵 ∈ 𝐴 ∧ 𝜒 ) ) ) |
14 |
9 13
|
sylibr |
⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) ) |
15 |
6 14
|
jca |
⊢ ( 𝜑 → ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → 𝑥 = 𝐵 ) ∧ ∀ 𝑥 ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) ) ) |
16 |
|
albiim |
⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ 𝑥 = 𝐵 ) ↔ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → 𝑥 = 𝐵 ) ∧ ∀ 𝑥 ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) ) ) |
17 |
15 16
|
sylibr |
⊢ ( 𝜑 → ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ 𝑥 = 𝐵 ) ) |
18 |
|
rabeqsn |
⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝐵 } ↔ ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ 𝑥 = 𝐵 ) ) |
19 |
17 18
|
sylibr |
⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝐵 } ) |