![]() |
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 1870 | . 2 ⊢ ∀𝑦𝜑 |
3 | 2 | ax-gen 1870 | 1 ⊢ ∀𝑥∀𝑦𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∀wal 1629 |
This theorem was proved from axioms: ax-gen 1870 |
This theorem is referenced by: bm1.1 2756 vtocl3 3413 eueq 3530 csbie2 3712 eusv1 4991 moop2 5093 mosubop 5104 eqrelriv 5351 opabid2 5388 xpidtr 5657 fvmptopab 6842 funoprab 6905 mpt2fun 6907 fnoprab 6908 elovmpt2 7024 wfrfun 7576 tfrlem7 7630 hartogs 8603 card2on 8613 epinid0 8659 cnvepnep 8665 tskwe 8974 ondomon 9585 fi1uzind 13474 brfi1indALT 13477 climeu 14487 letsr 17428 ulmdm 24360 wlkRes 26774 ajmoi 28047 helch 28433 hsn0elch 28438 chintcli 28523 adjmo 29024 nlelchi 29253 hmopidmchi 29343 bnj978 31350 bnj1052 31374 bnj1030 31386 frrlem5c 32116 fnsingle 32356 funimage 32365 funpartfun 32380 imagesset 32390 funtransport 32468 funray 32577 funline 32579 filnetlem3 32705 ax11-pm 33147 ax11-pm2 33151 bj-dfclel 33211 bj-dfcleq 33216 bj-snsetex 33275 wl-equsal1i 33657 mbfresfi 33781 riscer 34112 vvdifopab 34360 opabf 34465 cnvcosseq 34527 symrelcoss3 34550 cotrintab 38440 pm11.11 39092 fun2dmnopgexmpl 41819 |
Copyright terms: Public domain | W3C validator |