![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > gen2 | Structured version Visualization version GIF version |
Description: Generalization applied twice. (Contributed by NM, 30-Apr-1998.) |
Ref | Expression |
---|---|
gen2.1 | ⊢ 𝜑 |
Ref | Expression |
---|---|
gen2 | ⊢ ∀𝑥∀𝑦𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | gen2.1 | . . 3 ⊢ 𝜑 | |
2 | 1 | ax-gen 1790 | . 2 ⊢ ∀𝑦𝜑 |
3 | 2 | ax-gen 1790 | 1 ⊢ ∀𝑥∀𝑦𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∀wal 1532 |
This theorem was proved from axioms: ax-gen 1790 |
This theorem is referenced by: axextmo 2701 moeq 3700 csbie2 3933 mosneq 4841 eusv1 5387 moop2 5500 mosubop 5509 eqrelriv 5787 opabid2 5826 xpidtr 6126 fvmptopabOLD 7472 funoprab 7539 mpofunOLD 7542 fnoprab 7543 elovmpo 7663 wfrfunOLD 8341 tfrlem7 8405 hartogs 9580 card2on 9590 epinid0 9636 cnvepnep 9644 ssttrcl 9751 tskwe 9986 ondomon 10597 fi1uzind 14511 brfi1indALT 14514 climeu 15552 letsr 18613 ulmdm 26419 wlkResOLD 29584 ajmoi 30788 helch 31173 hsn0elch 31178 chintcli 31261 adjmo 31762 nlelchi 31991 hmopidmchi 32081 bnj978 34807 bnj1052 34833 bnj1030 34845 funen1cnv 34938 satfv0 35199 satfv0fun 35212 fnsingle 35756 funimage 35765 funpartfun 35780 imagesset 35790 funtransport 35868 funray 35977 funline 35979 filnetlem3 36105 bj-cbvalimi 36364 bj-cbveximi 36365 ax11-pm 36550 ax11-pm2 36554 bj-snsetex 36683 wl-equsal1i 37252 mbfresfi 37380 riscer 37702 vvdifopab 37971 opabf 38079 cnvcosseq 38148 antisymressn 38155 trressn 38156 symrelcoss3 38176 cotrintab 43318 pm11.11 44085 fun2dmnopgexmpl 46933 ichv 47057 ichf 47058 ichid 47059 icht 47060 ichcircshi 47062 icheq 47070 mof0ALT 48243 f1omo 48264 |
Copyright terms: Public domain | W3C validator |