| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nfra1 3283 | . 2
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 | 
| 2 |  | nfcv 2904 | . 2
⊢
Ⅎ𝑥𝐴 | 
| 3 |  | nfiu1 5026 | . 2
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵 | 
| 4 |  | simpr 484 | . . . . . . . . . . 11
⊢ (((𝑥 = 𝑦 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) | 
| 5 |  | rsp 3246 | . . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
𝐴 𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | 
| 6 | 5 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝑥 = 𝑦 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | 
| 7 |  | eleq1 2828 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) | 
| 8 | 7 | imbi2d 340 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐵))) | 
| 9 | 8 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑥 = 𝑦 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐵))) | 
| 10 | 6, 9 | mpbid 232 | . . . . . . . . . . . 12
⊢ ((𝑥 = 𝑦 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐵)) | 
| 11 | 10 | imp 406 | . . . . . . . . . . 11
⊢ (((𝑥 = 𝑦 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) | 
| 12 |  | rspe 3248 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) | 
| 13 | 4, 11, 12 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝑥 = 𝑦 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) | 
| 14 |  | abid 2717 | . . . . . . . . . 10
⊢ (𝑦 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) | 
| 15 | 13, 14 | sylibr 234 | . . . . . . . . 9
⊢ (((𝑥 = 𝑦 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}) | 
| 16 |  | eleq1 2828 | . . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ↔ 𝑦 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵})) | 
| 17 | 16 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝑥 = 𝑦 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ↔ 𝑦 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵})) | 
| 18 | 15, 17 | mpbird 257 | . . . . . . . 8
⊢ (((𝑥 = 𝑦 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}) | 
| 19 |  | df-iun 4992 | . . . . . . . 8
⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} | 
| 20 | 18, 19 | eleqtrrdi 2851 | . . . . . . 7
⊢ (((𝑥 = 𝑦 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ∪
𝑥 ∈ 𝐴 𝐵) | 
| 21 | 20 | expl 457 | . . . . . 6
⊢ (𝑥 = 𝑦 → ((∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) | 
| 22 | 21 | equcoms 2018 | . . . . 5
⊢ (𝑦 = 𝑥 → ((∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) | 
| 23 | 22 | vtocleg 3552 | . . . 4
⊢ (𝑥 ∈ 𝐴 → ((∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) | 
| 24 | 23 | anabsi7 671 | . . 3
⊢
((∀𝑥 ∈
𝐴 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ∪
𝑥 ∈ 𝐴 𝐵) | 
| 25 | 24 | ex 412 | . 2
⊢
(∀𝑥 ∈
𝐴 𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) | 
| 26 | 1, 2, 3, 25 | ssrd 3987 | 1
⊢
(∀𝑥 ∈
𝐴 𝑥 ∈ 𝐵 → 𝐴 ⊆ ∪
𝑥 ∈ 𝐴 𝐵) |