Users' Mathboxes Mathbox for Eric Schmidt < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  prclaxpr Structured version   Visualization version   GIF version

Theorem prclaxpr 44947
Description: A class that is closed under the pairing operation models the Axiom of Pairing ax-pr 5437. Lemma II.2.4(4) of [Kunen2] p. 111. (Contributed by Eric Schmidt, 29-Sep-2025.)
Assertion
Ref Expression
prclaxpr (∀𝑥𝑀𝑦𝑀 {𝑥, 𝑦} ∈ 𝑀 → ∀𝑥𝑀𝑦𝑀𝑧𝑀𝑤𝑀 ((𝑤 = 𝑥𝑤 = 𝑦) → 𝑤𝑧))
Distinct variable groups:   𝑥,𝑧,𝑤   𝑦,𝑧,𝑤   𝑧,𝑀
Allowed substitution hints:   𝑀(𝑥,𝑦,𝑤)

Proof of Theorem prclaxpr
StepHypRef Expression
1 vex 3481 . . . . . 6 𝑤 ∈ V
21elpr 4654 . . . . 5 (𝑤 ∈ {𝑥, 𝑦} ↔ (𝑤 = 𝑥𝑤 = 𝑦))
32biimpri 228 . . . 4 ((𝑤 = 𝑥𝑤 = 𝑦) → 𝑤 ∈ {𝑥, 𝑦})
43rgenw 3062 . . 3 𝑤𝑀 ((𝑤 = 𝑥𝑤 = 𝑦) → 𝑤 ∈ {𝑥, 𝑦})
5 eleq2 2827 . . . . . 6 (𝑧 = {𝑥, 𝑦} → (𝑤𝑧𝑤 ∈ {𝑥, 𝑦}))
65imbi2d 340 . . . . 5 (𝑧 = {𝑥, 𝑦} → (((𝑤 = 𝑥𝑤 = 𝑦) → 𝑤𝑧) ↔ ((𝑤 = 𝑥𝑤 = 𝑦) → 𝑤 ∈ {𝑥, 𝑦})))
76ralbidv 3175 . . . 4 (𝑧 = {𝑥, 𝑦} → (∀𝑤𝑀 ((𝑤 = 𝑥𝑤 = 𝑦) → 𝑤𝑧) ↔ ∀𝑤𝑀 ((𝑤 = 𝑥𝑤 = 𝑦) → 𝑤 ∈ {𝑥, 𝑦})))
87rspcev 3621 . . 3 (({𝑥, 𝑦} ∈ 𝑀 ∧ ∀𝑤𝑀 ((𝑤 = 𝑥𝑤 = 𝑦) → 𝑤 ∈ {𝑥, 𝑦})) → ∃𝑧𝑀𝑤𝑀 ((𝑤 = 𝑥𝑤 = 𝑦) → 𝑤𝑧))
94, 8mpan2 691 . 2 ({𝑥, 𝑦} ∈ 𝑀 → ∃𝑧𝑀𝑤𝑀 ((𝑤 = 𝑥𝑤 = 𝑦) → 𝑤𝑧))
1092ralimi 3120 1 (∀𝑥𝑀𝑦𝑀 {𝑥, 𝑦} ∈ 𝑀 → ∀𝑥𝑀𝑦𝑀𝑧𝑀𝑤𝑀 ((𝑤 = 𝑥𝑤 = 𝑦) → 𝑤𝑧))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 847   = wceq 1536  wcel 2105  wral 3058  wrex 3067  {cpr 4632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-v 3479  df-un 3967  df-sn 4631  df-pr 4633
This theorem is referenced by:  wfaxpr  44951
  Copyright terms: Public domain W3C validator