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 ( ∀ 𝑥𝑀𝑦𝑀 { 𝑥 , 𝑦 } ∈ 𝑀 → ∀ 𝑥𝑀𝑦𝑀𝑧𝑀𝑤𝑀 ( ( 𝑤 = 𝑥𝑤 = 𝑦 ) → 𝑤𝑧 ) )

Proof

Step Hyp Ref Expression
1 vex 𝑤 ∈ V
2 1 elpr ( 𝑤 ∈ { 𝑥 , 𝑦 } ↔ ( 𝑤 = 𝑥𝑤 = 𝑦 ) )
3 2 biimpri ( ( 𝑤 = 𝑥𝑤 = 𝑦 ) → 𝑤 ∈ { 𝑥 , 𝑦 } )
4 3 rgenw 𝑤𝑀 ( ( 𝑤 = 𝑥𝑤 = 𝑦 ) → 𝑤 ∈ { 𝑥 , 𝑦 } )
5 eleq2 ( 𝑧 = { 𝑥 , 𝑦 } → ( 𝑤𝑧𝑤 ∈ { 𝑥 , 𝑦 } ) )
6 5 imbi2d ( 𝑧 = { 𝑥 , 𝑦 } → ( ( ( 𝑤 = 𝑥𝑤 = 𝑦 ) → 𝑤𝑧 ) ↔ ( ( 𝑤 = 𝑥𝑤 = 𝑦 ) → 𝑤 ∈ { 𝑥 , 𝑦 } ) ) )
7 6 ralbidv ( 𝑧 = { 𝑥 , 𝑦 } → ( ∀ 𝑤𝑀 ( ( 𝑤 = 𝑥𝑤 = 𝑦 ) → 𝑤𝑧 ) ↔ ∀ 𝑤𝑀 ( ( 𝑤 = 𝑥𝑤 = 𝑦 ) → 𝑤 ∈ { 𝑥 , 𝑦 } ) ) )
8 7 rspcev ( ( { 𝑥 , 𝑦 } ∈ 𝑀 ∧ ∀ 𝑤𝑀 ( ( 𝑤 = 𝑥𝑤 = 𝑦 ) → 𝑤 ∈ { 𝑥 , 𝑦 } ) ) → ∃ 𝑧𝑀𝑤𝑀 ( ( 𝑤 = 𝑥𝑤 = 𝑦 ) → 𝑤𝑧 ) )
9 4 8 mpan2 ( { 𝑥 , 𝑦 } ∈ 𝑀 → ∃ 𝑧𝑀𝑤𝑀 ( ( 𝑤 = 𝑥𝑤 = 𝑦 ) → 𝑤𝑧 ) )
10 9 2ralimi ( ∀ 𝑥𝑀𝑦𝑀 { 𝑥 , 𝑦 } ∈ 𝑀 → ∀ 𝑥𝑀𝑦𝑀𝑧𝑀𝑤𝑀 ( ( 𝑤 = 𝑥𝑤 = 𝑦 ) → 𝑤𝑧 ) )