Theorem ralopabb

Description: Restricted universal quantification over an ordered-pair class abstraction. (Contributed by RP, 25-Sep-2024)

	Ref	Expression
Hypotheses	ralopabb.o	⊢ 𝑂 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
	ralopabb.p	⊢ ( 𝑜 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜓 ↔ 𝜒 ) )
Assertion	ralopabb	⊢ ( ∀ 𝑜 ∈ 𝑂 𝜓 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		ralopabb.o	⊢ 𝑂 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
2		ralopabb.p	⊢ ( 𝑜 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜓 ↔ 𝜒 ) )
3		2nalexn	⊢ ( ¬ ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜒 ) ↔ ∃ 𝑥 ∃ 𝑦 ¬ ( 𝜑 → 𝜒 ) )
4	2	notbid	⊢ ( 𝑜 = ⟨ 𝑥 , 𝑦 ⟩ → ( ¬ 𝜓 ↔ ¬ 𝜒 ) )
5	1 4	rexopabb	⊢ ( ∃ 𝑜 ∈ 𝑂 ¬ 𝜓 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝜑 ∧ ¬ 𝜒 ) )
6		annim	⊢ ( ( 𝜑 ∧ ¬ 𝜒 ) ↔ ¬ ( 𝜑 → 𝜒 ) )
7	6	2exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝜑 ∧ ¬ 𝜒 ) ↔ ∃ 𝑥 ∃ 𝑦 ¬ ( 𝜑 → 𝜒 ) )
8	5 7	bitri	⊢ ( ∃ 𝑜 ∈ 𝑂 ¬ 𝜓 ↔ ∃ 𝑥 ∃ 𝑦 ¬ ( 𝜑 → 𝜒 ) )
9		rexnal	⊢ ( ∃ 𝑜 ∈ 𝑂 ¬ 𝜓 ↔ ¬ ∀ 𝑜 ∈ 𝑂 𝜓 )
10	3 8 9	3bitr2ri	⊢ ( ¬ ∀ 𝑜 ∈ 𝑂 𝜓 ↔ ¬ ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜒 ) )
11	10	con4bii	⊢ ( ∀ 𝑜 ∈ 𝑂 𝜓 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜒 ) )