Metamath Proof Explorer

Theorem prclaxpr

Description: A class that is closed under the pairing operation models the Axiom of Pairing ax-pr . Lemma II.2.4(4) of Kunen2 p. 111. (Contributed by Eric Schmidt, 29-Sep-2025)

Ref Expression
Assertion prclaxpr ⊢ ∀ x ∈ M ∀ y ∈ M x y ∈ M → ∀ x ∈ M ∀ y ∈ M ∃ z ∈ M ∀ w ∈ M w = x ∨ w = y → w ∈ z

Proof

Step Hyp Ref Expression
1 vex ⊢ w ∈ V
2 1 elpr ⊢ w ∈ x y ↔ w = x ∨ w = y
3 2 biimpri ⊢ w = x ∨ w = y → w ∈ x y
4 3 rgenw ⊢ ∀ w ∈ M w = x ∨ w = y → w ∈ x y
5 eleq2 ⊢ z = x y → w ∈ z ↔ w ∈ x y
6 5 imbi2d ⊢ z = x y → w = x ∨ w = y → w ∈ z ↔ w = x ∨ w = y → w ∈ x y
7 6 ralbidv ⊢ z = x y → ∀ w ∈ M w = x ∨ w = y → w ∈ z ↔ ∀ w ∈ M w = x ∨ w = y → w ∈ x y
8 7 rspcev ⊢ x y ∈ M ∧ ∀ w ∈ M w = x ∨ w = y → w ∈ x y → ∃ z ∈ M ∀ w ∈ M w = x ∨ w = y → w ∈ z
9 4 8 mpan2 ⊢ x y ∈ M → ∃ z ∈ M ∀ w ∈ M w = x ∨ w = y → w ∈ z
10 9 2ralimi ⊢ ∀ x ∈ M ∀ y ∈ M x y ∈ M → ∀ x ∈ M ∀ y ∈ M ∃ z ∈ M ∀ w ∈ M w = x ∨ w = y → w ∈ z