Step |
Hyp |
Ref |
Expression |
1 |
|
nfopab1 |
⊢ Ⅎ 𝑥 { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } |
2 |
|
nfopab1 |
⊢ Ⅎ 𝑥 { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } |
3 |
1 2
|
nfss |
⊢ Ⅎ 𝑥 { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ⊆ { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } |
4 |
|
nfopab2 |
⊢ Ⅎ 𝑦 { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } |
5 |
|
nfopab2 |
⊢ Ⅎ 𝑦 { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } |
6 |
4 5
|
nfss |
⊢ Ⅎ 𝑦 { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ⊆ { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } |
7 |
|
ssel |
⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ⊆ { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } → ( 〈 𝑥 , 𝑦 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } → 〈 𝑥 , 𝑦 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ) ) |
8 |
|
opabid |
⊢ ( 〈 𝑥 , 𝑦 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ 𝜑 ) |
9 |
|
opabid |
⊢ ( 〈 𝑥 , 𝑦 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ↔ 𝜓 ) |
10 |
7 8 9
|
3imtr3g |
⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ⊆ { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } → ( 𝜑 → 𝜓 ) ) |
11 |
6 10
|
alrimi |
⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ⊆ { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } → ∀ 𝑦 ( 𝜑 → 𝜓 ) ) |
12 |
3 11
|
alrimi |
⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ⊆ { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } → ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) ) |
13 |
|
ssopab2 |
⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) → { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ⊆ { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ) |
14 |
12 13
|
impbii |
⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ⊆ { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ↔ ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) ) |