Step |
Hyp |
Ref |
Expression |
1 |
|
ssrabf.1 |
⊢ Ⅎ 𝑥 𝐵 |
2 |
|
ssrabf.2 |
⊢ Ⅎ 𝑥 𝐴 |
3 |
|
df-rab |
⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } |
4 |
3
|
sseq2i |
⊢ ( 𝐵 ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ↔ 𝐵 ⊆ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ) |
5 |
1
|
ssabf |
⊢ ( 𝐵 ⊆ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ) |
6 |
1 2
|
dfss3f |
⊢ ( 𝐵 ⊆ 𝐴 ↔ ∀ 𝑥 ∈ 𝐵 𝑥 ∈ 𝐴 ) |
7 |
6
|
anbi1i |
⊢ ( ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 𝜑 ) ↔ ( ∀ 𝑥 ∈ 𝐵 𝑥 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 𝜑 ) ) |
8 |
|
r19.26 |
⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( ∀ 𝑥 ∈ 𝐵 𝑥 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 𝜑 ) ) |
9 |
|
df-ral |
⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ) |
10 |
7 8 9
|
3bitr2ri |
⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ↔ ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 𝜑 ) ) |
11 |
4 5 10
|
3bitri |
⊢ ( 𝐵 ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ↔ ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 𝜑 ) ) |