| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-co 5694 | . 2
⊢
({〈𝑦, 𝑧〉 ∣ 𝜓} ∘ {〈𝑥, 𝑦〉 ∣ 𝜑}) = {〈𝑎, 𝑏〉 ∣ ∃𝑐(𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 ∧ 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏)} | 
| 2 |  | nfcv 2905 | . . . . . 6
⊢
Ⅎ𝑥𝑎 | 
| 3 |  | nfopab1 5213 | . . . . . 6
⊢
Ⅎ𝑥{〈𝑥, 𝑦〉 ∣ 𝜑} | 
| 4 |  | nfcv 2905 | . . . . . 6
⊢
Ⅎ𝑥𝑐 | 
| 5 | 2, 3, 4 | nfbr 5190 | . . . . 5
⊢
Ⅎ𝑥 𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 | 
| 6 |  | nfv 1914 | . . . . 5
⊢
Ⅎ𝑥 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏 | 
| 7 | 5, 6 | nfan 1899 | . . . 4
⊢
Ⅎ𝑥(𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 ∧ 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏) | 
| 8 | 7 | nfex 2324 | . . 3
⊢
Ⅎ𝑥∃𝑐(𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 ∧ 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏) | 
| 9 |  | nfv 1914 | . . . . 5
⊢
Ⅎ𝑧 𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 | 
| 10 |  | nfcv 2905 | . . . . . 6
⊢
Ⅎ𝑧𝑐 | 
| 11 |  | nfopab2 5214 | . . . . . 6
⊢
Ⅎ𝑧{〈𝑦, 𝑧〉 ∣ 𝜓} | 
| 12 |  | nfcv 2905 | . . . . . 6
⊢
Ⅎ𝑧𝑏 | 
| 13 | 10, 11, 12 | nfbr 5190 | . . . . 5
⊢
Ⅎ𝑧 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏 | 
| 14 | 9, 13 | nfan 1899 | . . . 4
⊢
Ⅎ𝑧(𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 ∧ 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏) | 
| 15 | 14 | nfex 2324 | . . 3
⊢
Ⅎ𝑧∃𝑐(𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 ∧ 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏) | 
| 16 |  | nfv 1914 | . . 3
⊢
Ⅎ𝑎∃𝑦(𝑥{〈𝑥, 𝑦〉 ∣ 𝜑}𝑦 ∧ 𝑦{〈𝑦, 𝑧〉 ∣ 𝜓}𝑧) | 
| 17 |  | nfv 1914 | . . 3
⊢
Ⅎ𝑏∃𝑦(𝑥{〈𝑥, 𝑦〉 ∣ 𝜑}𝑦 ∧ 𝑦{〈𝑦, 𝑧〉 ∣ 𝜓}𝑧) | 
| 18 |  | nfv 1914 | . . . 4
⊢
Ⅎ𝑦(𝑎 = 𝑥 ∧ 𝑏 = 𝑧) | 
| 19 |  | nfcv 2905 | . . . . . . 7
⊢
Ⅎ𝑦𝑎 | 
| 20 |  | nfopab2 5214 | . . . . . . 7
⊢
Ⅎ𝑦{〈𝑥, 𝑦〉 ∣ 𝜑} | 
| 21 |  | nfcv 2905 | . . . . . . 7
⊢
Ⅎ𝑦𝑐 | 
| 22 | 19, 20, 21 | nfbr 5190 | . . . . . 6
⊢
Ⅎ𝑦 𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 | 
| 23 |  | nfopab1 5213 | . . . . . . 7
⊢
Ⅎ𝑦{〈𝑦, 𝑧〉 ∣ 𝜓} | 
| 24 |  | nfcv 2905 | . . . . . . 7
⊢
Ⅎ𝑦𝑏 | 
| 25 | 21, 23, 24 | nfbr 5190 | . . . . . 6
⊢
Ⅎ𝑦 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏 | 
| 26 | 22, 25 | nfan 1899 | . . . . 5
⊢
Ⅎ𝑦(𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 ∧ 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏) | 
| 27 | 26 | a1i 11 | . . . 4
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑧) → Ⅎ𝑦(𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 ∧ 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏)) | 
| 28 |  | simpll 767 | . . . . . . 7
⊢ (((𝑎 = 𝑥 ∧ 𝑏 = 𝑧) ∧ 𝑐 = 𝑦) → 𝑎 = 𝑥) | 
| 29 |  | simpr 484 | . . . . . . 7
⊢ (((𝑎 = 𝑥 ∧ 𝑏 = 𝑧) ∧ 𝑐 = 𝑦) → 𝑐 = 𝑦) | 
| 30 | 28, 29 | breq12d 5156 | . . . . . 6
⊢ (((𝑎 = 𝑥 ∧ 𝑏 = 𝑧) ∧ 𝑐 = 𝑦) → (𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 ↔ 𝑥{〈𝑥, 𝑦〉 ∣ 𝜑}𝑦)) | 
| 31 |  | simplr 769 | . . . . . . 7
⊢ (((𝑎 = 𝑥 ∧ 𝑏 = 𝑧) ∧ 𝑐 = 𝑦) → 𝑏 = 𝑧) | 
| 32 | 29, 31 | breq12d 5156 | . . . . . 6
⊢ (((𝑎 = 𝑥 ∧ 𝑏 = 𝑧) ∧ 𝑐 = 𝑦) → (𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏 ↔ 𝑦{〈𝑦, 𝑧〉 ∣ 𝜓}𝑧)) | 
| 33 | 30, 32 | anbi12d 632 | . . . . 5
⊢ (((𝑎 = 𝑥 ∧ 𝑏 = 𝑧) ∧ 𝑐 = 𝑦) → ((𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 ∧ 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏) ↔ (𝑥{〈𝑥, 𝑦〉 ∣ 𝜑}𝑦 ∧ 𝑦{〈𝑦, 𝑧〉 ∣ 𝜓}𝑧))) | 
| 34 | 33 | ex 412 | . . . 4
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑧) → (𝑐 = 𝑦 → ((𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 ∧ 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏) ↔ (𝑥{〈𝑥, 𝑦〉 ∣ 𝜑}𝑦 ∧ 𝑦{〈𝑦, 𝑧〉 ∣ 𝜓}𝑧)))) | 
| 35 | 18, 27, 34 | cbvexdw 2341 | . . 3
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑧) → (∃𝑐(𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 ∧ 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏) ↔ ∃𝑦(𝑥{〈𝑥, 𝑦〉 ∣ 𝜑}𝑦 ∧ 𝑦{〈𝑦, 𝑧〉 ∣ 𝜓}𝑧))) | 
| 36 | 8, 15, 16, 17, 35 | cbvopab 5215 | . 2
⊢
{〈𝑎, 𝑏〉 ∣ ∃𝑐(𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 ∧ 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏)} = {〈𝑥, 𝑧〉 ∣ ∃𝑦(𝑥{〈𝑥, 𝑦〉 ∣ 𝜑}𝑦 ∧ 𝑦{〈𝑦, 𝑧〉 ∣ 𝜓}𝑧)} | 
| 37 |  | bj-opelopabid 37188 | . . . . 5
⊢ (𝑥{〈𝑥, 𝑦〉 ∣ 𝜑}𝑦 ↔ 𝜑) | 
| 38 |  | bj-opelopabid 37188 | . . . . 5
⊢ (𝑦{〈𝑦, 𝑧〉 ∣ 𝜓}𝑧 ↔ 𝜓) | 
| 39 | 37, 38 | anbi12i 628 | . . . 4
⊢ ((𝑥{〈𝑥, 𝑦〉 ∣ 𝜑}𝑦 ∧ 𝑦{〈𝑦, 𝑧〉 ∣ 𝜓}𝑧) ↔ (𝜑 ∧ 𝜓)) | 
| 40 | 39 | exbii 1848 | . . 3
⊢
(∃𝑦(𝑥{〈𝑥, 𝑦〉 ∣ 𝜑}𝑦 ∧ 𝑦{〈𝑦, 𝑧〉 ∣ 𝜓}𝑧) ↔ ∃𝑦(𝜑 ∧ 𝜓)) | 
| 41 | 40 | opabbii 5210 | . 2
⊢
{〈𝑥, 𝑧〉 ∣ ∃𝑦(𝑥{〈𝑥, 𝑦〉 ∣ 𝜑}𝑦 ∧ 𝑦{〈𝑦, 𝑧〉 ∣ 𝜓}𝑧)} = {〈𝑥, 𝑧〉 ∣ ∃𝑦(𝜑 ∧ 𝜓)} | 
| 42 | 1, 36, 41 | 3eqtri 2769 | 1
⊢
({〈𝑦, 𝑧〉 ∣ 𝜓} ∘ {〈𝑥, 𝑦〉 ∣ 𝜑}) = {〈𝑥, 𝑧〉 ∣ ∃𝑦(𝜑 ∧ 𝜓)} |