| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | relco 6126 | . . 3
⊢ Rel ( I
∘ 𝐵) | 
| 2 |  | relss 5791 | . . 3
⊢ (𝐴 ⊆ ( I ∘ 𝐵) → (Rel ( I ∘ 𝐵) → Rel 𝐴)) | 
| 3 | 1, 2 | mpi 20 | . 2
⊢ (𝐴 ⊆ ( I ∘ 𝐵) → Rel 𝐴) | 
| 4 |  | elrel 5808 | . . . . . 6
⊢ ((Rel
𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑦∃𝑧 𝑥 = 〈𝑦, 𝑧〉) | 
| 5 |  | vex 3484 | . . . . . . . . . . 11
⊢ 𝑦 ∈ V | 
| 6 |  | vex 3484 | . . . . . . . . . . 11
⊢ 𝑧 ∈ V | 
| 7 | 5, 6 | brco 5881 | . . . . . . . . . 10
⊢ (𝑦( I ∘ 𝐵)𝑧 ↔ ∃𝑥(𝑦𝐵𝑥 ∧ 𝑥 I 𝑧)) | 
| 8 | 6 | ideq 5863 | . . . . . . . . . . . 12
⊢ (𝑥 I 𝑧 ↔ 𝑥 = 𝑧) | 
| 9 | 8 | anbi1ci 626 | . . . . . . . . . . 11
⊢ ((𝑦𝐵𝑥 ∧ 𝑥 I 𝑧) ↔ (𝑥 = 𝑧 ∧ 𝑦𝐵𝑥)) | 
| 10 | 9 | exbii 1848 | . . . . . . . . . 10
⊢
(∃𝑥(𝑦𝐵𝑥 ∧ 𝑥 I 𝑧) ↔ ∃𝑥(𝑥 = 𝑧 ∧ 𝑦𝐵𝑥)) | 
| 11 |  | breq2 5147 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (𝑦𝐵𝑥 ↔ 𝑦𝐵𝑧)) | 
| 12 | 11 | equsexvw 2004 | . . . . . . . . . 10
⊢
(∃𝑥(𝑥 = 𝑧 ∧ 𝑦𝐵𝑥) ↔ 𝑦𝐵𝑧) | 
| 13 | 7, 10, 12 | 3bitri 297 | . . . . . . . . 9
⊢ (𝑦( I ∘ 𝐵)𝑧 ↔ 𝑦𝐵𝑧) | 
| 14 | 13 | a1i 11 | . . . . . . . 8
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝑦( I ∘ 𝐵)𝑧 ↔ 𝑦𝐵𝑧)) | 
| 15 |  | eleq1 2829 | . . . . . . . . 9
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝑥 ∈ ( I ∘ 𝐵) ↔ 〈𝑦, 𝑧〉 ∈ ( I ∘ 𝐵))) | 
| 16 |  | df-br 5144 | . . . . . . . . 9
⊢ (𝑦( I ∘ 𝐵)𝑧 ↔ 〈𝑦, 𝑧〉 ∈ ( I ∘ 𝐵)) | 
| 17 | 15, 16 | bitr4di 289 | . . . . . . . 8
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝑥 ∈ ( I ∘ 𝐵) ↔ 𝑦( I ∘ 𝐵)𝑧)) | 
| 18 |  | eleq1 2829 | . . . . . . . . 9
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝑥 ∈ 𝐵 ↔ 〈𝑦, 𝑧〉 ∈ 𝐵)) | 
| 19 |  | df-br 5144 | . . . . . . . . 9
⊢ (𝑦𝐵𝑧 ↔ 〈𝑦, 𝑧〉 ∈ 𝐵) | 
| 20 | 18, 19 | bitr4di 289 | . . . . . . . 8
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝑥 ∈ 𝐵 ↔ 𝑦𝐵𝑧)) | 
| 21 | 14, 17, 20 | 3bitr4d 311 | . . . . . . 7
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝑥 ∈ ( I ∘ 𝐵) ↔ 𝑥 ∈ 𝐵)) | 
| 22 | 21 | exlimivv 1932 | . . . . . 6
⊢
(∃𝑦∃𝑧 𝑥 = 〈𝑦, 𝑧〉 → (𝑥 ∈ ( I ∘ 𝐵) ↔ 𝑥 ∈ 𝐵)) | 
| 23 | 4, 22 | syl 17 | . . . . 5
⊢ ((Rel
𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ ( I ∘ 𝐵) ↔ 𝑥 ∈ 𝐵)) | 
| 24 | 23 | pm5.74da 804 | . . . 4
⊢ (Rel
𝐴 → ((𝑥 ∈ 𝐴 → 𝑥 ∈ ( I ∘ 𝐵)) ↔ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))) | 
| 25 | 24 | albidv 1920 | . . 3
⊢ (Rel
𝐴 → (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ ( I ∘ 𝐵)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))) | 
| 26 |  | df-ss 3968 | . . 3
⊢ (𝐴 ⊆ ( I ∘ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ ( I ∘ 𝐵))) | 
| 27 |  | df-ss 3968 | . . 3
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | 
| 28 | 25, 26, 27 | 3bitr4g 314 | . 2
⊢ (Rel
𝐴 → (𝐴 ⊆ ( I ∘ 𝐵) ↔ 𝐴 ⊆ 𝐵)) | 
| 29 | 3, 28 | biadanii 822 | 1
⊢ (𝐴 ⊆ ( I ∘ 𝐵) ↔ (Rel 𝐴 ∧ 𝐴 ⊆ 𝐵)) |