Step |
Hyp |
Ref |
Expression |
1 |
|
nfopdALT.1 |
⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 ) |
2 |
|
nfopdALT.2 |
⊢ ( 𝜑 → Ⅎ 𝑥 𝐵 ) |
3 |
|
abidnf |
⊢ ( Ⅎ 𝑥 𝐴 → { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } = 𝐴 ) |
4 |
3
|
adantr |
⊢ ( ( Ⅎ 𝑥 𝐴 ∧ Ⅎ 𝑥 𝐵 ) → { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } = 𝐴 ) |
5 |
|
abidnf |
⊢ ( Ⅎ 𝑥 𝐵 → { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐵 } = 𝐵 ) |
6 |
5
|
adantl |
⊢ ( ( Ⅎ 𝑥 𝐴 ∧ Ⅎ 𝑥 𝐵 ) → { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐵 } = 𝐵 ) |
7 |
4 6
|
opeq12d |
⊢ ( ( Ⅎ 𝑥 𝐴 ∧ Ⅎ 𝑥 𝐵 ) → 〈 { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } , { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐵 } 〉 = 〈 𝐴 , 𝐵 〉 ) |
8 |
|
nfaba1 |
⊢ Ⅎ 𝑥 { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } |
9 |
|
nfaba1 |
⊢ Ⅎ 𝑥 { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐵 } |
10 |
8 9
|
nfop |
⊢ Ⅎ 𝑥 〈 { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } , { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐵 } 〉 |
11 |
1 2 7 10
|
nfded2 |
⊢ ( 𝜑 → Ⅎ 𝑥 〈 𝐴 , 𝐵 〉 ) |