| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nfra1 3284 | . . . . . . . 8
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑡 ∈ 𝐵 | 
| 2 |  | nfv 1914 | . . . . . . . 8
⊢
Ⅎ𝑥 𝑡 ∈ 𝑧 | 
| 3 |  | eleq2 2830 | . . . . . . . 8
⊢ (𝑧 = 𝐵 → (𝑡 ∈ 𝑧 ↔ 𝑡 ∈ 𝐵)) | 
| 4 |  | vex 3484 | . . . . . . . . 9
⊢ 𝑧 ∈ V | 
| 5 | 4 | a1i 11 | . . . . . . . 8
⊢
(∀𝑥 ∈
𝐴 𝑡 ∈ 𝐵 → 𝑧 ∈ V) | 
| 6 |  | rspa 3248 | . . . . . . . 8
⊢
((∀𝑥 ∈
𝐴 𝑡 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑡 ∈ 𝐵) | 
| 7 | 1, 2, 3, 5, 6 | elabreximd 32529 | . . . . . . 7
⊢
((∀𝑥 ∈
𝐴 𝑡 ∈ 𝐵 ∧ 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) → 𝑡 ∈ 𝑧) | 
| 8 | 7 | ex 412 | . . . . . 6
⊢
(∀𝑥 ∈
𝐴 𝑡 ∈ 𝐵 → (𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) | 
| 9 | 8 | alrimiv 1927 | . . . . 5
⊢
(∀𝑥 ∈
𝐴 𝑡 ∈ 𝐵 → ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) | 
| 10 | 9 | adantl 481 | . . . 4
⊢
((∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝑡 ∈ 𝐵) → ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) | 
| 11 |  | nfra1 3284 | . . . . . 6
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 | 
| 12 | 2 | nfci 2893 | . . . . . . . . 9
⊢
Ⅎ𝑥𝑧 | 
| 13 |  | nfre1 3285 | . . . . . . . . . 10
⊢
Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 = 𝐵 | 
| 14 | 13 | nfab 2911 | . . . . . . . . 9
⊢
Ⅎ𝑥{𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} | 
| 15 | 12, 14 | nfel 2920 | . . . . . . . 8
⊢
Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} | 
| 16 | 15, 2 | nfim 1896 | . . . . . . 7
⊢
Ⅎ𝑥(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧) | 
| 17 | 16 | nfal 2323 | . . . . . 6
⊢
Ⅎ𝑥∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧) | 
| 18 | 11, 17 | nfan 1899 | . . . . 5
⊢
Ⅎ𝑥(∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) | 
| 19 |  | rspa 3248 | . . . . . . . . 9
⊢
((∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) | 
| 20 | 19 | elexd 3504 | . . . . . . . 8
⊢
((∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ V) | 
| 21 | 20 | adantlr 715 | . . . . . . 7
⊢
(((∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 ∧ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ V) | 
| 22 |  | simplr 769 | . . . . . . 7
⊢
(((∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 ∧ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) ∧ 𝑥 ∈ 𝐴) → ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) | 
| 23 |  | rspe 3249 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 = 𝐵) | 
| 24 |  | tbtru 1548 | . . . . . . . . . . . 12
⊢
(∃𝑥 ∈
𝐴 𝑦 = 𝐵 ↔ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ⊤)) | 
| 25 | 23, 24 | sylib 218 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ⊤)) | 
| 26 | 25 | ex 412 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ⊤))) | 
| 27 | 26 | alrimiv 1927 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ⊤))) | 
| 28 | 27 | adantl 481 | . . . . . . . 8
⊢
(((∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 ∧ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) ∧ 𝑥 ∈ 𝐴) → ∀𝑦(𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ⊤))) | 
| 29 |  | elabgt 3672 | . . . . . . . . 9
⊢ ((𝐵 ∈ V ∧ ∀𝑦(𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ⊤))) → (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ↔ ⊤)) | 
| 30 |  | tbtru 1548 | . . . . . . . . 9
⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ↔ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ↔ ⊤)) | 
| 31 | 29, 30 | sylibr 234 | . . . . . . . 8
⊢ ((𝐵 ∈ V ∧ ∀𝑦(𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ⊤))) → 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) | 
| 32 | 21, 28, 31 | syl2anc 584 | . . . . . . 7
⊢
(((∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 ∧ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) | 
| 33 |  | eleq1 2829 | . . . . . . . . . . 11
⊢ (𝑧 = 𝐵 → (𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})) | 
| 34 | 33, 3 | imbi12d 344 | . . . . . . . . . 10
⊢ (𝑧 = 𝐵 → ((𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧) ↔ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝐵))) | 
| 35 | 34 | spcgv 3596 | . . . . . . . . 9
⊢ (𝐵 ∈ V → (∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧) → (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝐵))) | 
| 36 | 35 | imp 406 | . . . . . . . 8
⊢ ((𝐵 ∈ V ∧ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) → (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝐵)) | 
| 37 | 36 | imp 406 | . . . . . . 7
⊢ (((𝐵 ∈ V ∧ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) ∧ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) → 𝑡 ∈ 𝐵) | 
| 38 | 21, 22, 32, 37 | syl21anc 838 | . . . . . 6
⊢
(((∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 ∧ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) ∧ 𝑥 ∈ 𝐴) → 𝑡 ∈ 𝐵) | 
| 39 | 38 | ex 412 | . . . . 5
⊢
((∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 ∧ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) → (𝑥 ∈ 𝐴 → 𝑡 ∈ 𝐵)) | 
| 40 | 18, 39 | ralrimi 3257 | . . . 4
⊢
((∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 ∧ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) → ∀𝑥 ∈ 𝐴 𝑡 ∈ 𝐵) | 
| 41 | 10, 40 | impbida 801 | . . 3
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 𝑡 ∈ 𝐵 ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧))) | 
| 42 | 41 | abbidv 2808 | . 2
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 → {𝑡 ∣ ∀𝑥 ∈ 𝐴 𝑡 ∈ 𝐵} = {𝑡 ∣ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)}) | 
| 43 |  | df-iin 4994 | . . 3
⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑡 ∣ ∀𝑥 ∈ 𝐴 𝑡 ∈ 𝐵} | 
| 44 | 43 | a1i 11 | . 2
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 → ∩
𝑥 ∈ 𝐴 𝐵 = {𝑡 ∣ ∀𝑥 ∈ 𝐴 𝑡 ∈ 𝐵}) | 
| 45 |  | df-int 4947 | . . 3
⊢ ∩ {𝑦
∣ ∃𝑥 ∈
𝐴 𝑦 = 𝐵} = {𝑡 ∣ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)} | 
| 46 | 45 | a1i 11 | . 2
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 → ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑡 ∣ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)}) | 
| 47 | 42, 44, 46 | 3eqtr4d 2787 | 1
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 → ∩
𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) |