Theorem ralbidar

Description: More general form of ralbida . (Contributed by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Hypotheses	ralbidar.1	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝜑 )
	ralbidar.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
Assertion	ralbidar	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ ∀ 𝑥 ∈ 𝐴 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		ralbidar.1	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝜑 )
2		ralbidar.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
3	2	ex	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝜓 ↔ 𝜒 ) ) )
4	3	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐴 → ( 𝜓 ↔ 𝜒 ) ) )
5	1 4	syl	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐴 → ( 𝜓 ↔ 𝜒 ) ) )
6		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐴 → ( 𝜓 ↔ 𝜒 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → ( 𝜓 ↔ 𝜒 ) ) ) )
7	5 6	sylib	⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → ( 𝜓 ↔ 𝜒 ) ) ) )
8		pm2.43	⊢ ( ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → ( 𝜓 ↔ 𝜒 ) ) ) → ( 𝑥 ∈ 𝐴 → ( 𝜓 ↔ 𝜒 ) ) )
9	8	pm5.74d	⊢ ( ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → ( 𝜓 ↔ 𝜒 ) ) ) → ( ( 𝑥 ∈ 𝐴 → 𝜓 ) ↔ ( 𝑥 ∈ 𝐴 → 𝜒 ) ) )
10	9	alimi	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → ( 𝜓 ↔ 𝜒 ) ) ) → ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 → 𝜓 ) ↔ ( 𝑥 ∈ 𝐴 → 𝜒 ) ) )
11		albi	⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 → 𝜓 ) ↔ ( 𝑥 ∈ 𝐴 → 𝜒 ) ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜓 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜒 ) ) )
12	7 10 11	3syl	⊢ ( 𝜑 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜓 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜒 ) ) )
13		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜓 ) )
14		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜒 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜒 ) )
15	12 13 14	3bitr4g	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ ∀ 𝑥 ∈ 𝐴 𝜒 ) )