This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem raleqbidvvOLD

Description: Obsolete version of raleqbidvv as of 9-Mar-2025. (Contributed by BJ, 22-Sep-2024) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses raleqbidvv.1 ⊢ ( 𝜑 → 𝐴 = 𝐵 )
raleqbidvv.2 ⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
Assertion raleqbidvvOLD ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ ∀ 𝑥 ∈ 𝐵 𝜒 ) )

Proof

Step Hyp Ref Expression
1 raleqbidvv.1 ⊢ ( 𝜑 → 𝐴 = 𝐵 )
2 raleqbidvv.2 ⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
3 2 alrimiv ⊢ ( 𝜑 → ∀ 𝑥 ( 𝜓 ↔ 𝜒 ) )
4 dfcleq ⊢ ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
5 1 4 sylib ⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
6 19.26 ⊢ ( ∀ 𝑥 ( ( 𝜓 ↔ 𝜒 ) ∧ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ) ↔ ( ∀ 𝑥 ( 𝜓 ↔ 𝜒 ) ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ) )
7 3 5 6 sylanbrc ⊢ ( 𝜑 → ∀ 𝑥 ( ( 𝜓 ↔ 𝜒 ) ∧ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ) )
8 imbi12 ⊢ ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) → ( ( 𝜓 ↔ 𝜒 ) → ( ( 𝑥 ∈ 𝐴 → 𝜓 ) ↔ ( 𝑥 ∈ 𝐵 → 𝜒 ) ) ) )
9 8 impcom ⊢ ( ( ( 𝜓 ↔ 𝜒 ) ∧ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ) → ( ( 𝑥 ∈ 𝐴 → 𝜓 ) ↔ ( 𝑥 ∈ 𝐵 → 𝜒 ) ) )
10 7 9 sylg ⊢ ( 𝜑 → ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 → 𝜓 ) ↔ ( 𝑥 ∈ 𝐵 → 𝜒 ) ) )
11 albi ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 → 𝜓 ) ↔ ( 𝑥 ∈ 𝐵 → 𝜒 ) ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜓 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝜒 ) ) )
12 10 11 syl ⊢ ( 𝜑 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜓 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝜒 ) ) )
13 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜓 ) )
14 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐵 𝜒 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝜒 ) )
15 12 13 14 3bitr4g ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ ∀ 𝑥 ∈ 𝐵 𝜒 ) )