Step |
Hyp |
Ref |
Expression |
1 |
|
eqrrabd.1 |
⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 ) |
2 |
|
eqrrabd.2 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐵 ↔ 𝜓 ) ) |
3 |
|
nfv |
⊢ Ⅎ 𝑥 𝜑 |
4 |
|
nfcv |
⊢ Ⅎ 𝑥 𝐵 |
5 |
|
nfrab1 |
⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝜓 } |
6 |
1
|
sseld |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴 ) ) |
7 |
6
|
pm4.71rd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) ) |
8 |
2
|
pm5.32da |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) ) |
9 |
7 8
|
bitrd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) ) |
10 |
|
rabid |
⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) |
11 |
9 10
|
bitr4di |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) ) |
12 |
3 4 5 11
|
eqrd |
⊢ ( 𝜑 → 𝐵 = { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) |