New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > gen2 | Unicode 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 1546 | . 2 |
3 | 2 | ax-gen 1546 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wal 1540 |
This theorem was proved from axioms: ax-gen 1546 |
This theorem is referenced by: euequ1 2292 bm1.1 2338 vtocl3 2911 eueq 3008 csbie2 3181 eqrelkriiv 4213 sikss1c1c 4267 ins2kss 4279 ins3kss 4280 nnsucelr 4428 ssfin 4470 ncfinlower 4483 mosubop 4613 eqoprriv 4853 fvopab4t 5385 1stfo 5505 2ndfo 5506 swapf1o 5511 funoprab 5584 fnoprab 5586 fnfullfunlem2 5857 fvfullfunlem2 5862 fvfullfunlem3 5863 xpassen 6057 |
Copyright terms: Public domain | W3C validator |