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 1787 | . 2 ⊢ ∀𝑦𝜑 |
3 | 2 | ax-gen 1787 | 1 ⊢ ∀𝑥∀𝑦𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∀wal 1526 |
This theorem was proved from axioms: ax-gen 1787 |
This theorem is referenced by: axextmo 2794 moeq 3695 csbie2 3919 mosneq 4765 eusv1 5282 moop2 5383 mosubop 5392 eqrelriv 5655 opabid2 5693 xpidtr 5975 fvmptopab 7198 funoprab 7263 mpofun 7265 fnoprab 7266 elovmpo 7379 wfrfun 7954 tfrlem7 8008 hartogs 8996 card2on 9006 epinid0 9052 cnvepnep 9059 tskwe 9367 ondomon 9973 fi1uzind 13843 brfi1indALT 13846 climeu 14900 letsr 17825 ulmdm 24908 wlkRes 27358 ajmoi 28562 helch 28947 hsn0elch 28952 chintcli 29035 adjmo 29536 nlelchi 29765 hmopidmchi 29855 bnj978 32120 bnj1052 32144 bnj1030 32156 funen1cnv 32254 satfv0 32502 satfv0fun 32515 fnsingle 33277 funimage 33286 funpartfun 33301 imagesset 33311 funtransport 33389 funray 33498 funline 33500 filnetlem3 33625 bj-cbvalimi 33877 bj-cbveximi 33878 ax11-pm 34052 ax11-pm2 34056 bj-snsetex 34172 wl-equsal1i 34664 mbfresfi 34819 riscer 35147 vvdifopab 35402 opabf 35500 cnvcosseq 35562 symrelcoss3 35585 cotrintab 39852 pm11.11 40583 fun2dmnopgexmpl 43360 ichv 43486 ichf 43487 ichid 43488 ichcircshi 43489 icheq 43497 |
Copyright terms: Public domain | W3C validator |