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 794. (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 796  1 
Colors of variables: wff set class 
Syntax hints: wi 4 wa 358 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 
This theorem depends on definitions: dfbi 177 dfan 360 
Copyright terms: Public domain  W3C validator 