P,Q:(Prop), f:({u:| P(u) }{v:| Q(v) }).
  Bij({u:| P(u) }; {v:| Q(v) }; f)
  
  (m:{u:| P(u) }, k:{v:| Q(v) }.
  (Bij({u:| P(u) & u = m }; {v:| Q(v) & v = k };
  (Bij(Replace value k by f(m) in f))

1

1. P : Prop 2. Q : Prop 3. f : {u:| P(u) }{v:| Q(v) } 4. Inj({u:| P(u) }; {v:| Q(v) }; f) 5. Surj({u:| P(u) }; {v:| Q(v) }; f) 6. m : {u:| P(u) } 7. k : {v:| Q(v) }   Bij({u:| P(u) & u = m }; {v:| Q(v) & v = k };   Bij(Replace value k by f(m) in f)

11 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html