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

Axiom ax-pr 3971
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 3905). (Contributed by NM, 14-Nov-2006.)
Assertion
Ref Expression
ax-pr  |-  E. z A. w ( ( w  =  x  \/  w  =  y )  ->  w  e.  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 1408 . . . . 5  wff  w  =  x
4 vy . . . . . 6  setvar  y
51, 4weq 1408 . . . . 5  wff  w  =  y
63, 5wo 639 . . . 4  wff  ( w  =  x  \/  w  =  y )
7 vz . . . . 5  setvar  z
81, 7wel 1410 . . . 4  wff  w  e.  z
96, 8wi 4 . . 3  wff  ( ( w  =  x  \/  w  =  y )  ->  w  e.  z )
109, 1wal 1257 . 2  wff  A. w
( ( w  =  x  \/  w  =  y )  ->  w  e.  z )
1110, 7wex 1397 1  wff  E. z A. w ( ( w  =  x  \/  w  =  y )  ->  w  e.  z )
Colors of variables: wff set class
This axiom is referenced by:  zfpair2  3972  bj-zfpair2  10396
  Copyright terms: Public domain W3C validator