Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-pr GIF version

Axiom ax-pr 3935
 Description: The Axiom of Pairing of IZF set theory. Axiom 2 of [Crosilla] p. "Axioms of CZF and IZF", except (a) unnecessary quantifiers are removed, and (b) Crosilla has a biconditional rather than an implication (but the two are equivalent by bm1.3ii 3869). (Contributed by NM, 14-Nov-2006.)
Assertion
Ref Expression
ax-pr zw((w = x w = y) → w z)
Distinct variable groups:   x,z,w   y,z,w

Detailed syntax breakdown of Axiom ax-pr
StepHypRef Expression
1 vw . . . . . 6 setvar w
2 vx . . . . . 6 setvar x
31, 2weq 1389 . . . . 5 wff w = x
4 vy . . . . . 6 setvar y
51, 4weq 1389 . . . . 5 wff w = y
63, 5wo 628 . . . 4 wff (w = x w = y)
7 vz . . . . 5 setvar z
81, 7wel 1391 . . . 4 wff w z
96, 8wi 4 . . 3 wff ((w = x w = y) → w z)
109, 1wal 1240 . 2 wff w((w = x w = y) → w z)
1110, 7wex 1378 1 wff zw((w = x w = y) → w z)
 Colors of variables: wff set class This axiom is referenced by:  zfpair2  3936  bj-zfpair2  9365
 Copyright terms: Public domain W3C validator