Proof of Theorem opabiota
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq2 6905 | . . 3
⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵)) | 
| 2 |  | opabiota.2 | . . . 4
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) | 
| 3 | 2 | iotabidv 6544 | . . 3
⊢ (𝑥 = 𝐵 → (℩𝑦𝜑) = (℩𝑦𝜓)) | 
| 4 | 1, 3 | eqeq12d 2752 | . 2
⊢ (𝑥 = 𝐵 → ((𝐹‘𝑥) = (℩𝑦𝜑) ↔ (𝐹‘𝐵) = (℩𝑦𝜓))) | 
| 5 |  | vex 3483 | . . . 4
⊢ 𝑥 ∈ V | 
| 6 | 5 | eldm 5910 | . . 3
⊢ (𝑥 ∈ dom 𝐹 ↔ ∃𝑦 𝑥𝐹𝑦) | 
| 7 |  | nfiota1 6515 | . . . . 5
⊢
Ⅎ𝑦(℩𝑦𝜑) | 
| 8 | 7 | nfeq2 2922 | . . . 4
⊢
Ⅎ𝑦(𝐹‘𝑥) = (℩𝑦𝜑) | 
| 9 |  | opabiota.1 | . . . . . . 7
⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ {𝑦 ∣ 𝜑} = {𝑦}} | 
| 10 | 9 | opabiotafun 6988 | . . . . . 6
⊢ Fun 𝐹 | 
| 11 |  | funbrfv 6956 | . . . . . 6
⊢ (Fun
𝐹 → (𝑥𝐹𝑦 → (𝐹‘𝑥) = 𝑦)) | 
| 12 | 10, 11 | ax-mp 5 | . . . . 5
⊢ (𝑥𝐹𝑦 → (𝐹‘𝑥) = 𝑦) | 
| 13 |  | df-br 5143 | . . . . . . . 8
⊢ (𝑥𝐹𝑦 ↔ 〈𝑥, 𝑦〉 ∈ 𝐹) | 
| 14 | 9 | eleq2i 2832 | . . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈ 𝐹 ↔ 〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ {𝑦 ∣ 𝜑} = {𝑦}}) | 
| 15 |  | opabidw 5528 | . . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ {𝑦 ∣ 𝜑} = {𝑦}} ↔ {𝑦 ∣ 𝜑} = {𝑦}) | 
| 16 | 13, 14, 15 | 3bitri 297 | . . . . . . 7
⊢ (𝑥𝐹𝑦 ↔ {𝑦 ∣ 𝜑} = {𝑦}) | 
| 17 |  | vsnid 4662 | . . . . . . . . 9
⊢ 𝑦 ∈ {𝑦} | 
| 18 |  | id 22 | . . . . . . . . 9
⊢ ({𝑦 ∣ 𝜑} = {𝑦} → {𝑦 ∣ 𝜑} = {𝑦}) | 
| 19 | 17, 18 | eleqtrrid 2847 | . . . . . . . 8
⊢ ({𝑦 ∣ 𝜑} = {𝑦} → 𝑦 ∈ {𝑦 ∣ 𝜑}) | 
| 20 |  | abid 2717 | . . . . . . . 8
⊢ (𝑦 ∈ {𝑦 ∣ 𝜑} ↔ 𝜑) | 
| 21 | 19, 20 | sylib 218 | . . . . . . 7
⊢ ({𝑦 ∣ 𝜑} = {𝑦} → 𝜑) | 
| 22 | 16, 21 | sylbi 217 | . . . . . 6
⊢ (𝑥𝐹𝑦 → 𝜑) | 
| 23 |  | vex 3483 | . . . . . . . . 9
⊢ 𝑦 ∈ V | 
| 24 | 5, 23 | breldm 5918 | . . . . . . . 8
⊢ (𝑥𝐹𝑦 → 𝑥 ∈ dom 𝐹) | 
| 25 | 9 | opabiotadm 6989 | . . . . . . . . 9
⊢ dom 𝐹 = {𝑥 ∣ ∃!𝑦𝜑} | 
| 26 | 25 | eqabri 2884 | . . . . . . . 8
⊢ (𝑥 ∈ dom 𝐹 ↔ ∃!𝑦𝜑) | 
| 27 | 24, 26 | sylib 218 | . . . . . . 7
⊢ (𝑥𝐹𝑦 → ∃!𝑦𝜑) | 
| 28 |  | iota1 6537 | . . . . . . 7
⊢
(∃!𝑦𝜑 → (𝜑 ↔ (℩𝑦𝜑) = 𝑦)) | 
| 29 | 27, 28 | syl 17 | . . . . . 6
⊢ (𝑥𝐹𝑦 → (𝜑 ↔ (℩𝑦𝜑) = 𝑦)) | 
| 30 | 22, 29 | mpbid 232 | . . . . 5
⊢ (𝑥𝐹𝑦 → (℩𝑦𝜑) = 𝑦) | 
| 31 | 12, 30 | eqtr4d 2779 | . . . 4
⊢ (𝑥𝐹𝑦 → (𝐹‘𝑥) = (℩𝑦𝜑)) | 
| 32 | 8, 31 | exlimi 2216 | . . 3
⊢
(∃𝑦 𝑥𝐹𝑦 → (𝐹‘𝑥) = (℩𝑦𝜑)) | 
| 33 | 6, 32 | sylbi 217 | . 2
⊢ (𝑥 ∈ dom 𝐹 → (𝐹‘𝑥) = (℩𝑦𝜑)) | 
| 34 | 4, 33 | vtoclga 3576 | 1
⊢ (𝐵 ∈ dom 𝐹 → (𝐹‘𝐵) = (℩𝑦𝜓)) |