Theorem mh-prprimbi

Description: Shortest possible version of ax-pr in primitive symbols. (Contributed by Matthew House, 13-Apr-2026)

	Ref	Expression
Assertion	mh-prprimbi	⊢ ( ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) ↔ ¬ ∀ 𝑧 ( 𝑥 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		jaob	⊢ ( ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) ↔ ( ( 𝑤 = 𝑥 → 𝑤 ∈ 𝑧 ) ∧ ( 𝑤 = 𝑦 → 𝑤 ∈ 𝑧 ) ) )
2	1	albii	⊢ ( ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) ↔ ∀ 𝑤 ( ( 𝑤 = 𝑥 → 𝑤 ∈ 𝑧 ) ∧ ( 𝑤 = 𝑦 → 𝑤 ∈ 𝑧 ) ) )
3		19.26	⊢ ( ∀ 𝑤 ( ( 𝑤 = 𝑥 → 𝑤 ∈ 𝑧 ) ∧ ( 𝑤 = 𝑦 → 𝑤 ∈ 𝑧 ) ) ↔ ( ∀ 𝑤 ( 𝑤 = 𝑥 → 𝑤 ∈ 𝑧 ) ∧ ∀ 𝑤 ( 𝑤 = 𝑦 → 𝑤 ∈ 𝑧 ) ) )
4		elequ1	⊢ ( 𝑤 = 𝑥 → ( 𝑤 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧 ) )
5	4	equsalvw	⊢ ( ∀ 𝑤 ( 𝑤 = 𝑥 → 𝑤 ∈ 𝑧 ) ↔ 𝑥 ∈ 𝑧 )
6		elequ1	⊢ ( 𝑤 = 𝑦 → ( 𝑤 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) )
7	6	equsalvw	⊢ ( ∀ 𝑤 ( 𝑤 = 𝑦 → 𝑤 ∈ 𝑧 ) ↔ 𝑦 ∈ 𝑧 )
8	5 7	anbi12i	⊢ ( ( ∀ 𝑤 ( 𝑤 = 𝑥 → 𝑤 ∈ 𝑧 ) ∧ ∀ 𝑤 ( 𝑤 = 𝑦 → 𝑤 ∈ 𝑧 ) ) ↔ ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑧 ) )
9	2 3 8	3bitri	⊢ ( ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) ↔ ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑧 ) )
10	9	exbii	⊢ ( ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) ↔ ∃ 𝑧 ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑧 ) )
11		exnalimn	⊢ ( ∃ 𝑧 ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑧 ) ↔ ¬ ∀ 𝑧 ( 𝑥 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑧 ) )
12	10 11	bitri	⊢ ( ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) ↔ ¬ ∀ 𝑧 ( 𝑥 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑧 ) )