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 2797 moeq 3697 csbie2 3921 mosneq 4767 eusv1 5283 moop2 5384 mosubop 5393 eqrelriv 5656 opabid2 5694 xpidtr 5976 fvmptopab 7198 funoprab 7263 mpofun 7265 fnoprab 7266 elovmpo 7379 wfrfun 7956 tfrlem7 8010 hartogs 8997 card2on 9007 epinid0 9053 cnvepnep 9060 tskwe 9368 ondomon 9974 fi1uzind 13845 brfi1indALT 13848 climeu 14902 letsr 17827 ulmdm 24910 wlkRes 27359 ajmoi 28563 helch 28948 hsn0elch 28953 chintcli 29036 adjmo 29537 nlelchi 29766 hmopidmchi 29856 bnj978 32121 bnj1052 32145 bnj1030 32157 funen1cnv 32255 satfv0 32503 satfv0fun 32516 fnsingle 33278 funimage 33287 funpartfun 33302 imagesset 33312 funtransport 33390 funray 33499 funline 33501 filnetlem3 33626 bj-cbvalimi 33878 bj-cbveximi 33879 ax11-pm 34053 ax11-pm2 34057 bj-snsetex 34173 wl-equsal1i 34665 mbfresfi 34820 riscer 35149 vvdifopab 35404 opabf 35502 cnvcosseq 35564 symrelcoss3 35587 cotrintab 39854 pm11.11 40586 fun2dmnopgexmpl 43364 ichv 43456 ichf 43457 ichid 43458 ichcircshi 43459 icheq 43467 |
Copyright terms: Public domain | W3C validator |