Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > axpr  Structured version Unicode version 
Description: The Axiom of Pairing of ZF set theory. It was derived as theorem axpr 4394 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily. (Contributed by NM, 14Nov2006.) 
Ref  Expression 

axpr 
Step  Hyp  Ref  Expression 

1  vw  . . . . . 6  
2  vx  . . . . . 6  
3  1, 2  weq 1653  . . . . 5 
4  vy  . . . . . 6  
5  1, 4  weq 1653  . . . . 5 
6  3, 5  wo 358  . . . 4 
7  vz  . . . . 5  
8  1, 7  wel 1726  . . . 4 
9  6, 8  wi 4  . . 3 
10  9, 1  wal 1549  . 2 
11  10, 7  wex 1550  1 
Colors of variables: wff set class 
This axiom is referenced by: zfpair2 4396 
Copyright terms: Public domain  W3C validator 