Proof of Theorem ssoprab2b
Step | Hyp | Ref
| Expression |
1 | | nfoprab1 6704 |
. . . 4
⊢
Ⅎ𝑥{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} |
2 | | nfoprab1 6704 |
. . . 4
⊢
Ⅎ𝑥{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} |
3 | 1, 2 | nfss 3596 |
. . 3
⊢
Ⅎ𝑥{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⊆ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} |
4 | | nfoprab2 6705 |
. . . . 5
⊢
Ⅎ𝑦{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} |
5 | | nfoprab2 6705 |
. . . . 5
⊢
Ⅎ𝑦{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} |
6 | 4, 5 | nfss 3596 |
. . . 4
⊢
Ⅎ𝑦{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⊆ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} |
7 | | nfoprab3 6706 |
. . . . . 6
⊢
Ⅎ𝑧{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} |
8 | | nfoprab3 6706 |
. . . . . 6
⊢
Ⅎ𝑧{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} |
9 | 7, 8 | nfss 3596 |
. . . . 5
⊢
Ⅎ𝑧{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⊆ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} |
10 | | ssel 3597 |
. . . . . 6
⊢
({〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} ⊆ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} → (〈〈𝑥, 𝑦〉, 𝑧〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} → 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓})) |
11 | | oprabid 6677 |
. . . . . 6
⊢
(〈〈𝑥,
𝑦〉, 𝑧〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜑) |
12 | | oprabid 6677 |
. . . . . 6
⊢
(〈〈𝑥,
𝑦〉, 𝑧〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} ↔ 𝜓) |
13 | 10, 11, 12 | 3imtr3g 284 |
. . . . 5
⊢
({〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} ⊆ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} → (𝜑 → 𝜓)) |
14 | 9, 13 | alrimi 2082 |
. . . 4
⊢
({〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} ⊆ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} → ∀𝑧(𝜑 → 𝜓)) |
15 | 6, 14 | alrimi 2082 |
. . 3
⊢
({〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} ⊆ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} → ∀𝑦∀𝑧(𝜑 → 𝜓)) |
16 | 3, 15 | alrimi 2082 |
. 2
⊢
({〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} ⊆ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} → ∀𝑥∀𝑦∀𝑧(𝜑 → 𝜓)) |
17 | | ssoprab2 6711 |
. 2
⊢
(∀𝑥∀𝑦∀𝑧(𝜑 → 𝜓) → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⊆ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓}) |
18 | 16, 17 | impbii 199 |
1
⊢
({〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} ⊆ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} ↔ ∀𝑥∀𝑦∀𝑧(𝜑 → 𝜓)) |