Description: Equality deduction for restricted universal quantification. (Contributed by Giovanni Mascellani, 10-Apr-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ralbi12f.1 | ⊢ Ⅎ 𝑥 𝐴 | |
ralbi12f.2 | ⊢ Ⅎ 𝑥 𝐵 | ||
Assertion | ralbi12f | ⊢ ( ( 𝐴 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝜓 ) ) → ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐵 𝜓 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralbi12f.1 | ⊢ Ⅎ 𝑥 𝐴 | |
2 | ralbi12f.2 | ⊢ Ⅎ 𝑥 𝐵 | |
3 | ralbi | ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝜓 ) → ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) | |
4 | 1 2 | raleqf | ⊢ ( 𝐴 = 𝐵 → ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ ∀ 𝑥 ∈ 𝐵 𝜓 ) ) |
5 | 3 4 | sylan9bbr | ⊢ ( ( 𝐴 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝜓 ) ) → ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐵 𝜓 ) ) |