![]() |
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 1798 | . 2 ⊢ ∀𝑦𝜑 |
3 | 2 | ax-gen 1798 | 1 ⊢ ∀𝑥∀𝑦𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∀wal 1540 |
This theorem was proved from axioms: ax-gen 1798 |
This theorem is referenced by: axextmo 2708 moeq 3703 csbie2 3935 mosneq 4843 eusv1 5389 moop2 5502 mosubop 5511 eqrelriv 5788 opabid2 5827 xpidtr 6121 fvmptopabOLD 7461 funoprab 7527 mpofunOLD 7530 fnoprab 7531 elovmpo 7648 wfrfunOLD 8316 tfrlem7 8380 hartogs 9536 card2on 9546 epinid0 9592 cnvepnep 9600 ssttrcl 9707 tskwe 9942 ondomon 10555 fi1uzind 14455 brfi1indALT 14458 climeu 15496 letsr 18543 ulmdm 25897 wlkResOLD 28897 ajmoi 30099 helch 30484 hsn0elch 30489 chintcli 30572 adjmo 31073 nlelchi 31302 hmopidmchi 31392 bnj978 33949 bnj1052 33975 bnj1030 33987 funen1cnv 34080 satfv0 34338 satfv0fun 34351 fnsingle 34880 funimage 34889 funpartfun 34904 imagesset 34914 funtransport 34992 funray 35101 funline 35103 filnetlem3 35254 bj-cbvalimi 35513 bj-cbveximi 35514 ax11-pm 35699 ax11-pm2 35703 bj-snsetex 35833 wl-equsal1i 36401 mbfresfi 36523 riscer 36845 vvdifopab 37117 opabf 37226 cnvcosseq 37296 antisymressn 37303 trressn 37304 symrelcoss3 37324 cotrintab 42351 pm11.11 43119 fun2dmnopgexmpl 45979 ichv 46104 ichf 46105 ichid 46106 icht 46107 ichcircshi 46109 icheq 46117 mof0ALT 47460 f1omo 47481 |
Copyright terms: Public domain | W3C validator |