Theorem abbibw

Description: Replace ax-10 , ax-11 , ax-12 in abbib with substitution hypotheses. (Contributed by SN, 27-May-2025)

	Ref	Expression
Hypotheses	abbibw.ph	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜃 ) )
	abbibw.ps	⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) )
Assertion	abbibw	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 } ↔ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		abbibw.ph	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜃 ) )
2		abbibw.ps	⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) )
3		dfcleq	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 } ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ 𝜓 } ) )
4		vex	⊢ 𝑦 ∈ V
5	4 1	elab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜃 )
6	4 2	elab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜓 } ↔ 𝜒 )
7	5 6	bibi12i	⊢ ( ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ 𝜓 } ) ↔ ( 𝜃 ↔ 𝜒 ) )
8	7	albii	⊢ ( ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ 𝜓 } ) ↔ ∀ 𝑦 ( 𝜃 ↔ 𝜒 ) )
9	1 2	bibi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ↔ 𝜓 ) ↔ ( 𝜃 ↔ 𝜒 ) ) )
10	9	bicomd	⊢ ( 𝑥 = 𝑦 → ( ( 𝜃 ↔ 𝜒 ) ↔ ( 𝜑 ↔ 𝜓 ) ) )
11	10	equcoms	⊢ ( 𝑦 = 𝑥 → ( ( 𝜃 ↔ 𝜒 ) ↔ ( 𝜑 ↔ 𝜓 ) ) )
12	11	cbvalvw	⊢ ( ∀ 𝑦 ( 𝜃 ↔ 𝜒 ) ↔ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) )
13	3 8 12	3bitri	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 } ↔ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) )