Description: Equality of the "Godel-set of universal quantification". (Contributed by AV, 18-Sep-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | goaleq12d.1 | ⊢ ( 𝜑 → 𝑀 = 𝑁 ) | |
goaleq12d.2 | ⊢ ( 𝜑 → 𝐴 = 𝐵 ) | ||
Assertion | goaleq12d | ⊢ ( 𝜑 → ∀𝑔 𝑀 𝐴 = ∀𝑔 𝑁 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | goaleq12d.1 | ⊢ ( 𝜑 → 𝑀 = 𝑁 ) | |
2 | goaleq12d.2 | ⊢ ( 𝜑 → 𝐴 = 𝐵 ) | |
3 | df-goal | ⊢ ∀𝑔 𝑀 𝐴 = ⟨ 2o , ⟨ 𝑀 , 𝐴 ⟩ ⟩ | |
4 | 3 | a1i | ⊢ ( 𝜑 → ∀𝑔 𝑀 𝐴 = ⟨ 2o , ⟨ 𝑀 , 𝐴 ⟩ ⟩ ) |
5 | 1 2 | opeq12d | ⊢ ( 𝜑 → ⟨ 𝑀 , 𝐴 ⟩ = ⟨ 𝑁 , 𝐵 ⟩ ) |
6 | 5 | opeq2d | ⊢ ( 𝜑 → ⟨ 2o , ⟨ 𝑀 , 𝐴 ⟩ ⟩ = ⟨ 2o , ⟨ 𝑁 , 𝐵 ⟩ ⟩ ) |
7 | df-goal | ⊢ ∀𝑔 𝑁 𝐵 = ⟨ 2o , ⟨ 𝑁 , 𝐵 ⟩ ⟩ | |
8 | 7 | eqcomi | ⊢ ⟨ 2o , ⟨ 𝑁 , 𝐵 ⟩ ⟩ = ∀𝑔 𝑁 𝐵 |
9 | 8 | a1i | ⊢ ( 𝜑 → ⟨ 2o , ⟨ 𝑁 , 𝐵 ⟩ ⟩ = ∀𝑔 𝑁 𝐵 ) |
10 | 6 9 | eqtrd | ⊢ ( 𝜑 → ⟨ 2o , ⟨ 𝑀 , 𝐴 ⟩ ⟩ = ∀𝑔 𝑁 𝐵 ) |
11 | 4 10 | eqtrd | ⊢ ( 𝜑 → ∀𝑔 𝑀 𝐴 = ∀𝑔 𝑁 𝐵 ) |