Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ref Structured version   Visualization version   GIF version

Definition df-ref 22117
 Description: Define the refinement relation. (Contributed by Jeff Hankins, 18-Jan-2010.)
Assertion
Ref Expression
df-ref Ref = {⟨𝑥, 𝑦⟩ ∣ ( 𝑦 = 𝑥 ∧ ∀𝑧𝑥𝑤𝑦 𝑧𝑤)}
Distinct variable group:   𝑥,𝑤,𝑦,𝑧

Detailed syntax breakdown of Definition df-ref
StepHypRef Expression
1 cref 22114 . 2 class Ref
2 vy . . . . . . 7 setvar 𝑦
32cv 1537 . . . . . 6 class 𝑦
43cuni 4800 . . . . 5 class 𝑦
5 vx . . . . . . 7 setvar 𝑥
65cv 1537 . . . . . 6 class 𝑥
76cuni 4800 . . . . 5 class 𝑥
84, 7wceq 1538 . . . 4 wff 𝑦 = 𝑥
9 vz . . . . . . . 8 setvar 𝑧
109cv 1537 . . . . . . 7 class 𝑧
11 vw . . . . . . . 8 setvar 𝑤
1211cv 1537 . . . . . . 7 class 𝑤
1310, 12wss 3881 . . . . . 6 wff 𝑧𝑤
1413, 11, 3wrex 3107 . . . . 5 wff 𝑤𝑦 𝑧𝑤
1514, 9, 6wral 3106 . . . 4 wff 𝑧𝑥𝑤𝑦 𝑧𝑤
168, 15wa 399 . . 3 wff ( 𝑦 = 𝑥 ∧ ∀𝑧𝑥𝑤𝑦 𝑧𝑤)
1716, 5, 2copab 5092 . 2 class {⟨𝑥, 𝑦⟩ ∣ ( 𝑦 = 𝑥 ∧ ∀𝑧𝑥𝑤𝑦 𝑧𝑤)}
181, 17wceq 1538 1 wff Ref = {⟨𝑥, 𝑦⟩ ∣ ( 𝑦 = 𝑥 ∧ ∀𝑧𝑥𝑤𝑦 𝑧𝑤)}
 Colors of variables: wff setvar class This definition is referenced by:  refrel  22120  isref  22121
 Copyright terms: Public domain W3C validator