| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | id 22 | . . . 4
⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵) | 
| 2 |  | dmeq 5913 | . . . 4
⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵) | 
| 3 | 1, 2 | feq12d 6723 | . . 3
⊢ (𝐴 = 𝐵 → (𝐴:dom 𝐴⟶On ↔ 𝐵:dom 𝐵⟶On)) | 
| 4 |  | ordeq 6390 | . . . 4
⊢ (dom
𝐴 = dom 𝐵 → (Ord dom 𝐴 ↔ Ord dom 𝐵)) | 
| 5 | 2, 4 | syl 17 | . . 3
⊢ (𝐴 = 𝐵 → (Ord dom 𝐴 ↔ Ord dom 𝐵)) | 
| 6 |  | fveq1 6904 | . . . . . . 7
⊢ (𝐴 = 𝐵 → (𝐴‘𝑥) = (𝐵‘𝑥)) | 
| 7 |  | fveq1 6904 | . . . . . . 7
⊢ (𝐴 = 𝐵 → (𝐴‘𝑦) = (𝐵‘𝑦)) | 
| 8 | 6, 7 | eleq12d 2834 | . . . . . 6
⊢ (𝐴 = 𝐵 → ((𝐴‘𝑥) ∈ (𝐴‘𝑦) ↔ (𝐵‘𝑥) ∈ (𝐵‘𝑦))) | 
| 9 | 8 | imbi2d 340 | . . . . 5
⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)) ↔ (𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦)))) | 
| 10 | 9 | 2ralbidv 3220 | . . . 4
⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)) ↔ ∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦)))) | 
| 11 | 2 | raleqdv 3325 | . . . . 5
⊢ (𝐴 = 𝐵 → (∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦)) ↔ ∀𝑦 ∈ dom 𝐵(𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦)))) | 
| 12 | 11 | ralbidv 3177 | . . . 4
⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦)) ↔ ∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐵(𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦)))) | 
| 13 | 2 | raleqdv 3325 | . . . 4
⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐵(𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦)) ↔ ∀𝑥 ∈ dom 𝐵∀𝑦 ∈ dom 𝐵(𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦)))) | 
| 14 | 10, 12, 13 | 3bitrd 305 | . . 3
⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)) ↔ ∀𝑥 ∈ dom 𝐵∀𝑦 ∈ dom 𝐵(𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦)))) | 
| 15 | 3, 5, 14 | 3anbi123d 1437 | . 2
⊢ (𝐴 = 𝐵 → ((𝐴:dom 𝐴⟶On ∧ Ord dom 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦))) ↔ (𝐵:dom 𝐵⟶On ∧ Ord dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐵∀𝑦 ∈ dom 𝐵(𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦))))) | 
| 16 |  | df-smo 8387 | . 2
⊢ (Smo
𝐴 ↔ (𝐴:dom 𝐴⟶On ∧ Ord dom 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)))) | 
| 17 |  | df-smo 8387 | . 2
⊢ (Smo
𝐵 ↔ (𝐵:dom 𝐵⟶On ∧ Ord dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐵∀𝑦 ∈ dom 𝐵(𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦)))) | 
| 18 | 15, 16, 17 | 3bitr4g 314 | 1
⊢ (𝐴 = 𝐵 → (Smo 𝐴 ↔ Smo 𝐵)) |