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

Definition df-ref 21118
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 21115 . 2 class Ref
2 vy . . . . . . 7 setvar 𝑦
32cv 1474 . . . . . 6 class 𝑦
43cuni 4372 . . . . 5 class 𝑦
5 vx . . . . . . 7 setvar 𝑥
65cv 1474 . . . . . 6 class 𝑥
76cuni 4372 . . . . 5 class 𝑥
84, 7wceq 1475 . . . 4 wff 𝑦 = 𝑥
9 vz . . . . . . . 8 setvar 𝑧
109cv 1474 . . . . . . 7 class 𝑧
11 vw . . . . . . . 8 setvar 𝑤
1211cv 1474 . . . . . . 7 class 𝑤
1310, 12wss 3540 . . . . . 6 wff 𝑧𝑤
1413, 11, 3wrex 2897 . . . . 5 wff 𝑤𝑦 𝑧𝑤
1514, 9, 6wral 2896 . . . 4 wff 𝑧𝑥𝑤𝑦 𝑧𝑤
168, 15wa 383 . . 3 wff ( 𝑦 = 𝑥 ∧ ∀𝑧𝑥𝑤𝑦 𝑧𝑤)
1716, 5, 2copab 4642 . 2 class {⟨𝑥, 𝑦⟩ ∣ ( 𝑦 = 𝑥 ∧ ∀𝑧𝑥𝑤𝑦 𝑧𝑤)}
181, 17wceq 1475 1 wff Ref = {⟨𝑥, 𝑦⟩ ∣ ( 𝑦 = 𝑥 ∧ ∀𝑧𝑥𝑤𝑦 𝑧𝑤)}
Colors of variables: wff setvar class
This definition is referenced by:  refrel  21121  isref  21122
  Copyright terms: Public domain W3C validator