Mathbox for Alan Sare 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > anabss7p1  Unicode version 
Description: A deduction unionizing a nonunionized collection of virtual hypotheses. This would have been named uun221 if the 0th permutation did not exist in set.mm as anabss7 795. (Contributed by Alan Sare, 4Feb2017.) (Proof modification is discouraged.) (New usage is discouraged.) 
Ref  Expression 

anabss7p1.1 
Ref  Expression 

anabss7p1 
Step  Hyp  Ref  Expression 

1  anabss7p1.1  . 2  
2  1  anabss3 797  1 
Colors of variables: wff set class 
Syntax hints: wi 4 wa 359 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 
This theorem depends on definitions: dfbi 178 dfan 361 
Copyright terms: Public domain  W3C validator 